Theorem pjclem1 10131

Description: Lemma for projection commutation theorem.

Hypotheses

Ref	Expression
pjclem1.1	|- G e. CH
pjclem1.2	|- H e. CH

Assertion

Ref	Expression
pjclem1	|- (G C_H H -> ((proj` G) o. (proj` H)) = (proj` (G i^i H)))

Proof of Theorem pjclem1

Step	Hyp	Ref	Expression
1		pjclem1.1	. . . . . 6 |- G e. CH
2		pjclem1.2	. . . . . 6 |- H e. CH
3	1, 2	cmbr 9540	. . . . 5 |- (G C_H H <-> G = ((G i^i H) vH (G i^i (_|_` H))))
4		fveq2 3738	. . . . 5 |- (G = ((G i^i H) vH (G i^i (_|_` H))) -> (proj` G) = (proj` ((G i^i H) vH (G i^i (_|_` H)))))
5	3, 4	sylbi 199	. . . 4 |- (G C_H H -> (proj` G) = (proj` ((G i^i H) vH (G i^i (_|_` H)))))
6		inss2 2240	. . . . . . . 8 |- (G i^i H) (_ H
7	1	choccl 9192	. . . . . . . . . 10 |- (_|_` G) e. CH
8	2, 7	chub2 9400	. . . . . . . . 9 |- H (_ ((_|_` G) vH H)
9	1, 2	chdmm3 9409	. . . . . . . . 9 |- (_|_` (G i^i (_|_` H))) = ((_|_` G) vH H)
10	8, 9	sseqtr4 2103	. . . . . . . 8 |- H (_ (_|_` (G i^i (_|_` H)))
11	6, 10	sstri 2082	. . . . . . 7 |- (G i^i H) (_ (_|_` (G i^i (_|_` H)))
12	1, 2	chincl 9390	. . . . . . . 8 |- (G i^i H) e. CH
13	2	choccl 9192	. . . . . . . . 9 |- (_|_` H) e. CH
14	1, 13	chincl 9390	. . . . . . . 8 |- (G i^i (_|_` H)) e. CH
15	12, 14	pjscj 10105	. . . . . . 7 |- ((G i^i H) (_ (_|_` (G i^i (_|_` H))) -> (proj` ((G i^i H) vH (G i^i (_|_` H)))) = ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H)))))
16	11, 15	ax-mp 7	. . . . . 6 |- (proj` ((G i^i H) vH (G i^i (_|_` H)))) = ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))
17	16	eqeq2i 1492	. . . . 5 |- ((proj` G) = (proj` ((G i^i H) vH (G i^i (_|_` H)))) <-> (proj` G) = ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H)))))
18		coeq2 3296	. . . . . 6 |- ((proj` G) = ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H)))) -> ((proj` H) o. (proj` G)) = ((proj` H) o. ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))))
19	12	pjf 9656	. . . . . . . . . 10 |- (proj` (G i^i H)):H~-->H~
20	14	pjf 9656	. . . . . . . . . 10 |- (proj` (G i^i (_|_` H))):H~-->H~
21	2, 19, 20	pjsdi 10090	. . . . . . . . 9 |- ((proj` H) o. ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))) = (((proj` H) o. (proj` (G i^i H))) +op ((proj` H) o. (proj` (G i^i (_|_` H)))))
22	12, 2	pjss1co 10098	. . . . . . . . . . 11 |- ((G i^i H) (_ H <-> ((proj` H) o. (proj` (G i^i H))) = (proj` (G i^i H)))
23	6, 22	mpbi 189	. . . . . . . . . 10 |- ((proj` H) o. (proj` (G i^i H))) = (proj` (G i^i H))
24	2, 14	pjorthco 10104	. . . . . . . . . . 11 |- (H (_ (_|_` (G i^i (_|_` H))) -> ((proj` H) o. (proj` (G i^i (_|_` H)))) = 0hop)
25	10, 24	ax-mp 7	. . . . . . . . . 10 |- ((proj` H) o. (proj` (G i^i (_|_` H)))) = 0hop
26	23, 25	opreq12i 3987	. . . . . . . . 9 |- (((proj` H) o. (proj` (G i^i H))) +op ((proj` H) o. (proj` (G i^i (_|_` H))))) = ((proj` (G i^i H)) +op 0hop)
27	19	hoaddid1 9719	. . . . . . . . 9 |- ((proj` (G i^i H)) +op 0hop) = (proj` (G i^i H))
28	21, 26, 27	3eqtr 1506	. . . . . . . 8 |- ((proj` H) o. ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))) = (proj` (G i^i H))
29	28	eqeq2i 1492	. . . . . . 7 |- (((proj` H) o. (proj` G)) = ((proj` H) o. ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))) <-> ((proj` H) o. (proj` G)) = (proj` (G i^i H)))
30		coeq2 3296	. . . . . . . 8 |- (((proj` H) o. (proj` G)) = (proj` (G i^i H)) -> ((proj` G) o. ((proj` H) o. (proj` G))) = ((proj` G) o. (proj` (G i^i H))))
31		inss1 2239	. . . . . . . . 9 |- (G i^i H) (_ G
32	12, 1	pjss1co 10098	. . . . . . . . 9 |- ((G i^i H) (_ G <-> ((proj` G) o. (proj` (G i^i H))) = (proj` (G i^i H)))
33	31, 32	mpbi 189	. . . . . . . 8 |- ((proj` G) o. (proj` (G i^i H))) = (proj` (G i^i H))
34	30, 33	syl6eq 1530	. . . . . . 7 |- (((proj` H) o. (proj` G)) = (proj` (G i^i H)) -> ((proj` G) o. ((proj` H) o. (proj` G))) = (proj` (G i^i H)))
35	29, 34	sylbi 199	. . . . . 6 |- (((proj` H) o. (proj` G)) = ((proj` H) o. ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H))))) -> ((proj` G) o. ((proj` H) o. (proj` G))) = (proj` (G i^i H)))
36	18, 35	syl 10	. . . . 5 |- ((proj` G) = ((proj` (G i^i H)) +op (proj` (G i^i (_|_` H)))) -> ((proj` G) o. ((proj` H) o. (proj` G))) = (proj` (G i^i H)))
37	17, 36	sylbi 199	. . . 4 |- ((proj` G) = (proj` ((G i^i H) vH (G i^i (_|_` H)))) -> ((proj` G) o. ((proj` H) o. (proj` G))) = (proj` (G i^i H)))
38	5, 37	syl 10	. . 3 |- (G C_H H -> ((proj` G) o. ((proj` H) o. (proj` G))) = (proj` (G i^i H)))
39	1, 2	cmcm3 9544	. . . . 5 |- (G C_H H <-> (_|_` G) C_H H)
40	7, 2	cmbr 9540	. . . . 5 |- ((_|_` G) C_H H <-> (_|_` G) = (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H))))
41	39, 40	bitr 173	. . . 4 |- (G C_H H <-> (_|_` G) = (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H))))
42		fveq2 3738	. . . . 5 |- ((_|_` G) = (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H))) -> (proj` (_|_` G)) = (proj` (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H)))))
43		inss2 2240	. . . . . . . . 9 |- ((_|_` G) i^i H) (_ H
44	2, 1	chub2 9400	. . . . . . . . . 10 |- H (_ (G vH H)
45	1, 2	chdmm4 9410	. . . . . . . . . 10 |- (_|_` ((_|_` G) i^i (_|_` H))) = (G vH H)
46	44, 45	sseqtr4 2103	. . . . . . . . 9 |- H (_ (_|_` ((_|_` G) i^i (_|_` H)))
47	43, 46	sstri 2082	. . . . . . . 8 |- ((_|_` G) i^i H) (_ (_|_` ((_|_` G) i^i (_|_` H)))
48	7, 2	chincl 9390	. . . . . . . . 9 |- ((_|_` G) i^i H) e. CH
49	7, 13	chincl 9390	. . . . . . . . 9 |- ((_|_` G) i^i (_|_` H)) e. CH
50	48, 49	pjscj 10105	. . . . . . . 8 |- (((_|_` G) i^i H) (_ (_|_` ((_|_` G) i^i (_|_` H))) -> (proj` (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H)))) = ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H)))))
51	47, 50	ax-mp 7	. . . . . . 7 |- (proj` (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H)))) = ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H))))
52	51	eqeq2i 1492	. . . . . 6 |- ((proj` (_|_` G)) = (proj` (((_|_` G) i^i H) vH ((_|_` G) i^i (_|_` H)))) <-> (proj` (_|_` G)) = ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H)))))
53		coeq2 3296	. . . . . . 7 |- ((proj` (_|_` G)) = ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H)))) -> ((proj` H) o. (proj` (_|_` G))) = ((proj` H) o. ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H))))))
54	48	pjf 9656	. . . . . . . . . . 11 |- (proj` ((_|_` G) i^i H)):H~-->H~
55	49	pjf 9656	. . . . . . . . . . 11 |- (proj` ((_|_` G) i^i (_|_` H))):H~-->H~
56	2, 54, 55	pjsdi 10090	. . . . . . . . . 10 |- ((proj` H) o. ((proj` ((_|_` G) i^i H)) +op (proj` ((_|_` G) i^i (_|_` H))))) = (((proj` H) o. (proj` ((_|_` G