cdj1 - Hilbert Space Explorer

Home

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem cdj1 10360

Description: Two ways to express "

and

are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520.

**Hypotheses**
Ref	Expression
cdj1.1
cdj1.2

**Assertion**
Ref	Expression
cdj1	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem cdj1**
Step	Hyp	Ref	Expression
1		gt0ne0t 5618	. . . . . . 7 $/\$
2		rerecclt 5803	. . . . . . 7 $/\$
3	1, 2	syldan 467	. . . . . 6 $/\$
4	3	adantrr 395	. . . . 5 $/\$ $/\$
5		recgt0t 5861	. . . . . . 7 $/\$
6	5	adantrr 395	. . . . . 6 $/\$ $/\$
7		1re 5435	. . . . . . . . . . . . . . . . . . 19
8	7	a1i 8	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
9		cdj1.2	. . . . . . . . . . . . . . . . . . . . . . . 24
10	9	shel 9082	. . . . . . . . . . . . . . . . . . . . . . 23
11		ax1cn 5269	. . . . . . . . . . . . . . . . . . . . . . . . 25
12	11	negcl 5369	. . . . . . . . . . . . . . . . . . . . . . . 24
13		hvmulclt 8883	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
14	12, 13	mpan 695	. . . . . . . . . . . . . . . . . . . . . . 23
15	10, 14	syl 10	. . . . . . . . . . . . . . . . . . . . . 22
16		normclt 8991	. . . . . . . . . . . . . . . . . . . . . 22
17	15, 16	syl 10	. . . . . . . . . . . . . . . . . . . . 21
18	17	adantl 388	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
19		axaddrcl 5272	. . . . . . . . . . . . . . . . . . . . 21 $/\$
20	7, 19	mpan 695	. . . . . . . . . . . . . . . . . . . 20
21	18, 20	syl 10	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
22	21	adantr 389	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
23		axmulrcl 5274	. . . . . . . . . . . . . . . . . . . . 21 $/\$
24		hvsubclt 8887	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
25		cdj1.1	. . . . . . . . . . . . . . . . . . . . . . . 24
26	25	shel 9082	. . . . . . . . . . . . . . . . . . . . . . 23
27	24, 26, 10	syl2an 454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
28		normclt 8991	. . . . . . . . . . . . . . . . . . . . . 22
29	27, 28	syl 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
30	23, 29	sylan2 451	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
31	30	anassrs 441	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
32	31	adantr 389	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
33		addge01t 5672	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
34	7, 33	mpan 695	. . . . . . . . . . . . . . . . . . . . 21
35	34	biimpa 416	. . . . . . . . . . . . . . . . . . . 20 $/\$
36		normge0t 8992	. . . . . . . . . . . . . . . . . . . . 21
37	15, 36	syl 10	. . . . . . . . . . . . . . . . . . . 20
38	35, 17, 37	sylanc 471	. . . . . . . . . . . . . . . . . . 19
39	38	ad2antlr 405	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
40		shmulcltOLD 9088	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
41	9, 40	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
42	12, 41	mpan 695	. . . . . . . . . . . . . . . . . . . . . 22
43		fveq2 3724	. . . . . . . . . . . . . . . . . . . . . . . . 25
44	43	opreq2d 3976	. . . . . . . . . . . . . . . . . . . . . . . 24
45		opreq2 3969	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	46	opreq2d 3976	. . . . . . . . . . . . . . . . . . . . . . . 24
48	44, 47	breq12d 2631	. . . . . . . . . . . . . . . . . . . . . . 23
49	48	rcla4v 1873	. . . . . . . . . . . . . . . . . . . . . 22
50	42, 49	syl 10	. . . . . . . . . . . . . . . . . . . . 21
51	50	imp 350	. . . . . . . . . . . . . . . . . . . 20 $/\$
52	51	ad2ant2lr 410	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53		opreq1 3968	. . . . . . . . . . . . . . . . . . . . 21
54	53	eqcoms 1478	. . . . . . . . . . . . . . . . . . . 20