mdsymlem6 - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem mdsymlem6 10330

Description: Lemma for mdsym 10333. 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 groups:

**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 10329	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
5		sseq1 2085	. . . . . . . . . . . . . . . . . . . . . . . 24
6		sstr2 2074	. . . . . . . . . . . . . . . . . . . . . . . . 25
7		chinclt 9417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
8	2, 7	mpan2 698	. . . . . . . . . . . . . . . . . . . . . . . . . 26
9		chub2t 9426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
10	1, 9	mpan 697	. . . . . . . . . . . . . . . . . . . . . . . . . 26
11	8, 10	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25
12	6, 11	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . 24
13	5, 12	syl6bi 214	. . . . . . . . . . . . . . . . . . . . . . 23
14	13	imp3a 361	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
15	14	a1i 8	. . . . . . . . . . . . . . . . . . . . 21 $/\$
16	15	com13 33	. . . . . . . . . . . . . . . . . . . 20 $/\$
17	16	adantrr 397	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
18	17	ad2ant2r 411	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
19	18	adantll 394	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
20	19	com12 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
21	20	exp3a 376	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	4, 21	pm2.61d2 129	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
23	22	r19.23aivv 1751	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	23	com12 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	24	imim2d 25	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	25	com34 36	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	26	imp4b 365	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	1, 2	chjcom 9386	. . . . . . . . . . . 12
29	28	sseq2i 2089	. . . . . . . . . . 11
30	29	anbi2i 482	. . . . . . . . . 10 $/\$ $/\$
31		ssin 2235	. . . . . . . . . 10 $/\$
32	30, 31	bitr 173	. . . . . . . . 9 $/\$
33	27, 32	syl5ibr 207	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	ex 373	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
35	34	r19.20dva 1712	. . . . . 6 $/\$ $/\$ $/\$
36		chrelat3t 10293	. . . . . . . 8 $/\$
37	2, 1	chjcl 9375	. . . . . . . . 9
38		chinclt 9417	. . . . . . . . 9 $/\$
39	37, 38	mpan2 698	. . . . . . . 8
40		chjclt 9324	. . . . . . . . . 10 $/\$
41	1, 40	mpan2 698	. . . . . . . . 9
42	8, 41	syl 10	. . . . . . . 8
43	36, 39, 42	sylanc 473	. . . . . . 7
44	43	adantr 391	. . . . . 6 $/\$
45	35, 44	sylibrd 204	. . . . 5 $/\$ $/\$ $/\$
46	45	ex 373	. . . 4 $/\$ $/\$