Theorem pjclem4 5653

Description: Lemma for projection commutation theorem.

Hypotheses

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

Assertion

Ref	Expression
pjclem4	|- (((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) -> ((Proj` G) o. (Proj` H)) = (Proj` (G i^i H)))

Proof of Theorem pjclem4

Step	Hyp	Ref	Expression
1		pjclem1.1	. . . . . . . 8 |- G e. CH
2		pjclem1.2	. . . . . . . 8 |- H e. CH
3	1, 2	chincl 5382	. . . . . . 7 |- (G i^i H) e. CH
4	3	pjv 5589	. . . . . 6 |- (((((Proj` G) o. (Proj` H))` x) e. (G i^i H) /\ (x -v (((Proj` G) o. (Proj` H))` x)) e. (_|_` (G i^i H))) -> ((Proj` (G i^i H))` ((((Proj` G) o. (Proj` H))` x) +v (x -v (((Proj` G) o. (Proj` H))` x)))) = (((Proj` G) o. (Proj` H))` x))
5	1, 2	pjcocl 5629	. . . . . . . . 9 |- (x e. H~ -> (((Proj` G) o. (Proj` H))` x) e. G)
6	5	adantl 305	. . . . . . . 8 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ x e. H~) -> (((Proj` G) o. (Proj` H))` x) e. G)
7		fveq1 2831	. . . . . . . . . . 11 |- (((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) -> (((Proj` G) o. (Proj` H))` x) = (((Proj` H) o. (Proj` G))` x))
8	7	eleq1d 1155	. . . . . . . . . 10 |- (((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) -> ((((Proj` G) o. (Proj` H))` x) e. H <-> (((Proj` H) o. (Proj` G))` x) e. H))
9	2, 1	pjcocl 5629	. . . . . . . . . 10 |- (x e. H~ -> (((Proj` H) o. (Proj` G))` x) e. H)
10	8, 9	syl5bir 184	. . . . . . . . 9 |- (((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) -> (x e. H~ -> (((Proj` G) o. (Proj` H))` x) e. H))
11	10	imp 277	. . . . . . . 8 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ x e. H~) -> (((Proj` G) o. (Proj` H))` x) e. H)
12	6, 11	jca 236	. . . . . . 7 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ x e. H~) -> ((((Proj` G) o. (Proj` H))` x) e. G /\ (((Proj` G) o. (Proj` H))` x) e. H))
13		elin 1635	. . . . . . 7 |- ((((Proj` G) o. (Proj` H))` x) e. (G i^i H) <-> ((((Proj` G) o. (Proj` H))` x) e. G /\ (((Proj` G) o. (Proj` H))` x) e. H))
14	12, 13	sylibr 175	. . . . . 6 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ x e. H~) -> (((Proj` G) o. (Proj` H))` x) e. (G i^i H))
15	1, 2	pjcohcl 5630	. . . . . . . . . 10 |- (x e. H~ -> (((Proj` G) o. (Proj` H))` x) e. H~)
16		hvsubclt 4998	. . . . . . . . . 10 |- ((x e. H~ /\ (((Proj` G) o. (Proj` H))` x) e. H~) -> (x -v (((Proj` G) o. (Proj` H))` x)) e. H~)
17	15, 16	mpdan 527	. . . . . . . . 9 |- (x e. H~ -> (x -v (((Proj` G) o. (Proj` H))` x)) e. H~)
18	17	adantl 305	. . . . . . . 8 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ x e. H~) -> (x -v (((Proj` G) o. (Proj` H))` x)) e. H~)
19		pm3.26 256	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. (G i^i H)) -> x e. H~)
20	15	adantr 306	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. (G i^i H)) -> (((Proj` G) o. (Proj` H))` x) e. H~)
21	3	chel 5137	. . . . . . . . . . . . . . . 16 |- (y e. (G i^i H) -> y e. H~)
22	21	adantl 305	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. (G i^i H)) -> y e. H~)
23	19, 20, 22	3jca 604	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> (x e. H~ /\ (((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~))
24	23	adantl 305	. . . . . . . . . . . . 13 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> (x e. H~ /\ (((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~))
25		his2subt 5052	. . . . . . . . . . . . 13 |- ((x e. H~ /\ (((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~) -> ((x -v (((Proj` G) o. (Proj` H))` x)) .i y) = ((x .i y) - ((((Proj` G) o. (Proj` H))` x) .i y)))
26	24, 25	syl 12	. . . . . . . . . . . 12 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((x -v (((Proj` G) o. (Proj` H))` x)) .i y) = ((x .i y) - ((((Proj` G) o. (Proj` H))` x) .i y)))
27	7	opreq1d 3012	. . . . . . . . . . . . . . 15 |- (((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) -> ((((Proj` G) o. (Proj` H))` x) .i y) = ((((Proj` H) o. (Proj` G))` x) .i y))
28	2, 1	pjadjco 5631	. . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ y e. H~) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (x .i (((Proj` G) o. (Proj` H))` y)))
29	28, 21	sylan2 346	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (x .i (((Proj` G) o. (Proj` H))` y)))
30	1, 2	pjclem4a 5652	. . . . . . . . . . . . . . . . . 18 |- (y e. (G i^i H) -> (((Proj` G) o. (Proj` H))` y) = y)
31	30	opreq2d 3013	. . . . . . . . . . . . . . . . 17 |- (y e. (G i^i H) -> (x .i (((Proj` G) o. (Proj` H))` y)) = (x .i y))
32	31	adantl 305	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ y e. (G i^i H)) -> (x .i (((Proj` G) o. (Proj` H))` y)) = (x .i y))
33	29, 32	eqtrd 1128	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (x .i y))
34	27, 33	sylan9eq 1144	. . . . . . . . . . . . . 14 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((((Proj` G) o. (Proj` H))` x) .i y) = (x .i y))
35	34	opreq1d 3012	. . . . . . . . . . . . 13 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> (((((Proj` G) o. (Proj` H))` x) .i y) - ((((Proj` G) o. (Proj` H))` x) .i y)) = ((x .i y) - ((((Proj` G) o. (Proj` H))` x) .i y)))
36	15, 21	anim12i 268	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~))
37	36	adantl 305	. . . . . . . . . . . . . 14 |- ((((Proj` G) o. (Proj` H)) = ((Proj` H) o. (Proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~))
38		ax-hicl 5043	. . . . . . . . . . . . . 14 |- (((((Proj` G) o. (Proj` H))` x) e. H~ /\ y e. H~) -> ((((Proj` G) o. (Proj` H))` x) .i y) e. CC)
39		subidt 4159	. . . . . . . . . . . . . 14 |- (((((Proj` G) o. (Proj` H))` x) .i y) e. CC -> (((((Proj` G) o. (Proj` H))` x) .i y) - ((((Proj` G) o. (Proj` H))` x) .i y)) = 0)
40	37, 38, 39	3syl 21	. . . . . . . . . . . . 13 |- ((((Proj`