Theorem pjclem4 10037

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	. . . . . . 7 |- G e. CH
2		pjclem1.2	. . . . . . 7 |- H e. CH
3	1, 2	chincl 9298	. . . . . 6 |- (G i^i H) e. CH
4	3	pjv 9567	. . . . 5 |- (((((proj` G) o. (proj` H))` x) e. (G i^i H) /\ (x -h (((proj` G) o. (proj` H))` x)) e. (_|_` (G i^i H))) -> ((proj` (G i^i H))` ((((proj` G) o. (proj` H))` x) +h (x -h (((proj` G) o. (proj` H))` x)))) = (((proj` G) o. (proj` H))` x))
5	1, 2	pjcocl 9998	. . . . . . . 8 |- (x e. H~ -> (((proj` G) o. (proj` H))` x) e. G)
6	5	adantl 388	. . . . . . 7 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ x e. H~) -> (((proj` G) o. (proj` H))` x) e. G)
7		fveq1 3708	. . . . . . . . . 10 |- (((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 1532	. . . . . . . . 9 |- (((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 9998	. . . . . . . . 9 |- (x e. H~ -> (((proj` H) o. (proj` G))` x) e. H)
10	8, 9	syl5bir 210	. . . . . . . 8 |- (((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) -> (x e. H~ -> (((proj` G) o. (proj` H))` x) e. H))
11	10	imp 350	. . . . . . 7 |- ((((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 288	. . . . . 6 |- ((((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 2197	. . . . . 6 |- ((((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 200	. . . . 5 |- ((((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 9999	. . . . . . . . 9 |- (x e. H~ -> (((proj` G) o. (proj` H))` x) e. H~)
16		hvsubclt 8808	. . . . . . . . 9 |- ((x e. H~ /\ (((proj` G) o. (proj` H))` x) e. H~) -> (x -h (((proj` G) o. (proj` H))` x)) e. H~)
17	15, 16	mpdan 702	. . . . . . . 8 |- (x e. H~ -> (x -h (((proj` G) o. (proj` H))` x)) e. H~)
18	17	adantl 388	. . . . . . 7 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ x e. H~) -> (x -h (((proj` G) o. (proj` H))` x)) e. H~)
19		pm3.26 319	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> x e. H~)
20	15	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> (((proj` G) o. (proj` H))` x) e. H~)
21	3	chel 9023	. . . . . . . . . . . . . . 15 |- (y e. (G i^i H) -> y e. H~)
22	21	adantl 388	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> y e. H~)
23	19, 20, 22	3jca 817	. . . . . . . . . . . . 13 |- ((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 388	. . . . . . . . . . . 12 |- ((((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 8879	. . . . . . . . . . . 12 |- ((x e. H~ /\ (((proj` G) o. (proj` H))` x) e. H~ /\ y e. H~) -> ((x -h (((proj` G) o. (proj` H))` x)) .ih y) = ((x .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)))
26	24, 25	syl 10	. . . . . . . . . . 11 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((x -h (((proj` G) o. (proj` H))` x)) .ih y) = ((x .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)))
27	7	opreq1d 3960	. . . . . . . . . . . . 13 |- (((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) -> ((((proj` G) o. (proj` H))` x) .ih y) = ((((proj` H) o. (proj` G))` x) .ih y))
28	2, 1	pjadjco 10000	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ y e. H~) -> ((((proj` H) o. (proj` G))` x) .ih y) = (x .ih (((proj` G) o. (proj` H))` y)))
29	28, 21	sylan2 451	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((proj` H) o. (proj` G))` x) .ih y) = (x .ih (((proj` G) o. (proj` H))` y)))
30	1, 2	pjclem4a 10036	. . . . . . . . . . . . . . . 16 |- (y e. (G i^i H) -> (((proj` G) o. (proj` H))` y) = y)
31	30	opreq2d 3961	. . . . . . . . . . . . . . 15 |- (y e. (G i^i H) -> (x .ih (((proj` G) o. (proj` H))` y)) = (x .ih y))
32	31	adantl 388	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> (x .ih (((proj` G) o. (proj` H))` y)) = (x .ih y))
33	29, 32	eqtrd 1499	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((proj` H) o. (proj` G))` x) .ih y) = (x .ih y))
34	27, 33	sylan9eq 1519	. . . . . . . . . . . 12 |- ((((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) .ih y) = (x .ih y))
35	34	opreq1d 3960	. . . . . . . . . . 11 |- ((((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) .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)) = ((x .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)))
36	15, 21	anim12i 333	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((proj` G) o. (proj` H))` x) e. H~ /\ y e. H~))
37	36	adantl 388	. . . . . . . . . . . 12 |- ((((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		hiclt 8868	. . . . . . . . . . . 12 |- (((((proj` G) o. (proj` H))` x) e. H~ /\ y e. H~) -> ((((proj` G) o. (proj` H))` x) .ih y) e. CC)
39		subidt 5367	. . . . . . . . . . . 12 |- (((((proj` G) o. (proj` H))` x) .ih y) e. CC -> (((((proj` G) o. (proj` H))` x) .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)) = 0)
40	37, 38, 39	3syl 20	. . . . . . . . . . 11 |- ((((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) .ih y) - ((((proj` G) o. (proj` H))` x) .ih y)) = 0)
41	26, 35, 40	3eqtr2d 1505	. . . . . . . . . 10 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((x -h (((proj`