Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pjclem1 5649

Description: Lemma for projection commutation theorem.

**Hypotheses**
Ref	Expression
pjclem1.1
pjclem1.2

**Assertion**
Ref	Expression
pjclem1

**Proof of Theorem pjclem1**
Step	Hyp	Ref	Expression
1		pjclem1.1	. . . . . 6
2		pjclem1.2	. . . . . 6
3	1, 2	cmbr 5499	. . . . 5
4		fveq2 2832	. . . . 5
5	3, 4	sylbi 174	. . . 4
6		inss2 1658	. . . . . . . 8
7	1	chocl 5192	. . . . . . . . . 10
8	2, 7	chub2 5391	. . . . . . . . 9
9	1, 2	chdmm3 5400	. . . . . . . . 9
10	8, 9	sseqtr4 1533	. . . . . . . 8
11	6, 10	sstri 1512	. . . . . . 7
12	1, 2	chincl 5382	. . . . . . . 8
13	2	chocl 5192	. . . . . . . . 9
14	1, 13	chincl 5382	. . . . . . . 8
15	12, 14	pjscj 5640	. . . . . . 7
16	11, 15	ax-mp 6	. . . . . 6
17	16	cleq2i 1111	. . . . 5
18		coeq2 2503	. . . . . 6
19	12	pjf 5588	. . . . . . . . . 10
20	14	pjf 5588	. . . . . . . . . 10
21	2, 19, 20	pjsdi 5625	. . . . . . . . 9
22	12, 2	pjss1co 5633	. . . . . . . . . . 11
23	6, 22	mpbi 164	. . . . . . . . . 10
24	2, 14	pjorthco 5639	. . . . . . . . . . 11
25	10, 24	ax-mp 6	. . . . . . . . . 10
26	23, 25	opreq12i 3011	. . . . . . . . 9
27	19	hoid0 5614	. . . . . . . . 9
28	21, 26, 27	3eqtr 1123	. . . . . . . 8
29	28	cleq2i 1111	. . . . . . 7
30		coeq2 2503	. . . . . . . 8
31		inss1 1657	. . . . . . . . 9
32	12, 1	pjss1co 5633	. . . . . . . . 9
33	31, 32	mpbi 164	. . . . . . . 8
34	30, 33	syl6eq 1140	. . . . . . 7
35	29, 34	sylbi 174	. . . . . 6
36	18, 35	syl 12	. . . . 5
37	17, 36	sylbi 174	. . . 4
38	5, 37	syl 12	. . 3
39	1, 2	cmcm3 5503	. . . . 5
40	7, 2	cmbr 5499	. . . . 5
41	39, 40	bitr 151	. . . 4
42		fveq2 2832	. . . . 5
43		inss2 1658	. . . . . . . . 9
44	2, 1	chub2 5391	. . . . . . . . . 10
45	1, 2	chdmm4 5401	. . . . . . . . . 10
46	44, 45	sseqtr4 1533	. . . . . . . . 9
47	43, 46	sstri 1512	. . . . . . . 8
48	7, 2	chincl 5382	. . . . . . . . 9
49	7, 13	chincl 5382	. . . . . . . . 9
50	48, 49	pjscj 5640	. . . . . . . 8
51	47, 50	ax-mp 6	. . . . . . 7
52	51	cleq2i 1111	. . . . . 6
53		coeq2 2503	. . . . . . 7
54	48	pjf 5588	. . . . . . . . . . 11