Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem mdsymlem6 5781

Description: Lemma for mdsym 5784. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167.

**Hypotheses**
Ref	Expression
mdsymlem1.1
mdsymlem1.2
mdsymlem1.3

**Assertion**
Ref	Expression
mdsymlem6	$/\$ $/\$

Distinct variable group(s):

**Proof of Theorem mdsymlem6**
Step	Hyp	Ref	Expression
1		mdsymlem1.1	. . . . . . . . . . . . . . . 16
2		mdsymlem1.2	. . . . . . . . . . . . . . . 16
3		mdsymlem1.3	. . . . . . . . . . . . . . . 16
4	1, 2, 3	mdsymlem5 5780	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
5		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . 25
6		sstr2 1510	. . . . . . . . . . . . . . . . . . . . . . . . . 26
7		chinclt 5416	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
8	2, 7	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
9		chub2t 5425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
10	1, 9	mpan 518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
11	8, 10	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26
12	6, 11	syl5 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
13	5, 12	syl6bi 187	. . . . . . . . . . . . . . . . . . . . . . . 24
14	13	imp3a 279	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
15	14	a1i 7	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
16	15	com13 33	. . . . . . . . . . . . . . . . . . . . 21 $/\$
17	16	adantrr 312	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
18	17	adantrr 312	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19	18	adantlr 310	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
20	19	adantll 309	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
21	20	com12 13	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
22	21	exp3a 292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
23	4, 22	pm2.61d2 111	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
24	23	r19.23aivv 1287	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
25	24	com12 13	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
26	25	syl3d 26	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
27	26	com34 36	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
28	27	imp4b 283	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	1, 2	chjcom 5389	. . . . . . . . . . . 12
30	29	sseq2i 1525	. . . . . . . . . . 11
31	30	anbi2i 367	. . . . . . . . . 10 $/\$ $/\$
32		ssin 1659	. . . . . . . . . 10 $/\$
33	31, 32	bitr 151	. . . . . . . . 9 $/\$
34	28, 33	syl5ibr 182	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	exp 291	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
36	35	r19.20dva 1256	. . . . . 6 $/\$ $/\$ $/\$
37		chrelat3t 5762	. . . . . . . 8 $/\$
38	2, 1	chjcl 5379	. . . . . . . . 9
39		chinclt 5416	. . . . . . . . 9 $/\$
40	38, 39	mpan2 519	. . . . . . . 8
41		chjclt 5330	. . . . . . . . . 10 $/\$
42	1, 41	mpan2 519	. . . . . . . . 9
43	8, 42	syl 12	. . . . . . . 8
44	37, 40, 43	sylanc 361	. . . . . . 7
45	44	adantr 306	. . . . . 6 $/\$
46	36, 45	sylibrd 179	. . . . 5 $/\$ $/\$ $/\$
47	46	exp 291	. . . 4