Theorem pjclem4 10211

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	chincli 9466	. . . . . 6 |- (G i^i H) e. CH
4	3	pjvi 9733	. . . . 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	pjcocli 10170	. . . . . . . 8 |- (x e. H~ -> (((proj` G) o. (proj` H))` x) e. G)
6	5	adantl 397	. . . . . . 7 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ x e. H~) -> (((proj` G) o. (proj` H))` x) e. G)
7		fveq1 3780	. . . . . . . . . 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 1587	. . . . . . . . 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	pjcocli 10170	. . . . . . . . 9 |- (x e. H~ -> (((proj` H) o. (proj` G))` x) e. H)
10	8, 9	syl5bir 217	. . . . . . . 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 357	. . . . . . 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 295	. . . . . 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 2258	. . . . . 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 207	. . . . 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	pjcohcli 10171	. . . . . . . . 9 |- (x e. H~ -> (((proj` G) o. (proj` H))` x) e. H~)
16		hvsubcl 8970	. . . . . . . . 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 716	. . . . . . . 8 |- (x e. H~ -> (x -h (((proj` G) o. (proj` H))` x)) e. H~)
18	17	adantl 397	. . . . . . 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 326	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> x e. H~)
20	15	adantr 398	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> (((proj` G) o. (proj` H))` x) e. H~)
21	3	cheli 9185	. . . . . . . . . . . . . . 15 |- (y e. (G i^i H) -> y e. H~)
22	21	adantl 397	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. (G i^i H)) -> y e. H~)
23	19, 20, 22	3jca 831	. . . . . . . . . . . . 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 397	. . . . . . . . . . . 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		his2sub 9041	. . . . . . . . . . . 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 4033	. . . . . . . . . . . . 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	pjadjcoi 10172	. . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . 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 10210	. . . . . . . . . . . . . . . 16 |- (y e. (G i^i H) -> (((proj` G) o. (proj` H))` y) = y)
31	30	opreq2d 4034	. . . . . . . . . . . . . . 15 |- (y e. (G i^i H) -> (x .ih (((proj` G) o. (proj` H))` y)) = (x .ih y))
32	31	adantl 397	. . . . . . . . . . . . . 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 1554	. . . . . . . . . . . . 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 1574	. . . . . . . . . . . 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 4033	. . . . . . . . . . 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 340	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. (G i^i H)) -> ((((proj` G) o. (proj` H))` x) e. H~ /\ y e. H~))
37	36	adantl 397	. . . . . . . . . . . 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		hicl 9030	. . . . . . . . . . . 12 |- (((((proj` G) o. (proj` H))` x) e. H~ /\ y e. H~) -> ((((proj` G) o. (proj` H))` x) .ih y) e. CC)
39		subid 5460	. . . . . . . . . . . 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 1560	. . . . . . . . . 10 |- ((((proj` G) o. (proj` H)) = ((proj` H) o. (proj` G)) /\ (x e. H~ /\ y e. (G i^i H))) -> ((x -h (((proj