Theorem pj3cor1 10137

Description: Projection triplet corollary.

Hypotheses

Ref	Expression
pjadj2co.1	|- F e. CH
pjadj2co.2	|- G e. CH
pjadj2co.3	|- H e. CH

Assertion

Ref	Expression
pj3cor1	|- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` F)) o. (proj` G)))

Proof of Theorem pj3cor1

Step	Hyp	Ref	Expression
1		fveq1 3723	. . . . . . . . . . 11 |- ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)) -> ((((proj` F) o. (proj` G)) o. (proj` H))` y) = ((((proj` G) o. (proj` F)) o. (proj` H))` y))
2	1	opreq2d 3976	. . . . . . . . . 10 |- ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)) -> (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)) = (x .ih ((((proj` G) o. (proj` F)) o. (proj` H))` y)))
3	2	adantl 388	. . . . . . . . 9 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)) = (x .ih ((((proj` G) o. (proj` F)) o. (proj` H))` y)))
4	3	ad2antlr 405	. . . . . . . 8 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)) = (x .ih ((((proj` G) o. (proj` F)) o. (proj` H))` y)))
5		pjadj2co.1	. . . . . . . . . . . . 13 |- F e. CH
6		pjadj2co.2	. . . . . . . . . . . . 13 |- G e. CH
7	5, 6	chincl 9383	. . . . . . . . . . . 12 |- (F i^i G) e. CH
8		pjadj2co.3	. . . . . . . . . . . 12 |- H e. CH
9	7, 8	chincl 9383	. . . . . . . . . . 11 |- ((F i^i G) i^i H) e. CH
10	9	pjadjt 9630	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (((proj` ((F i^i G) i^i H))` x) .ih y) = (x .ih ((proj` ((F i^i G) i^i H))` y)))
11	10	adantlr 393	. . . . . . . . 9 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (((proj` ((F i^i G) i^i H))` x) .ih y) = (x .ih ((proj` ((F i^i G) i^i H))` y)))
12	5, 6, 8	pj3 10136	. . . . . . . . . . . 12 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> (((proj` F) o. (proj` G)) o. (proj` H)) = (proj` ((F i^i G) i^i H)))
13	12	fveq1d 3726	. . . . . . . . . . 11 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) = ((proj` ((F i^i G) i^i H))` x))
14	13	opreq1d 3975	. . . . . . . . . 10 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) .ih y) = (((proj` ((F i^i G) i^i H))` x) .ih y))
15	14	ad2antlr 405	. . . . . . . . 9 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) .ih y) = (((proj` ((F i^i G) i^i H))` x) .ih y))
16	12	fveq1d 3726	. . . . . . . . . . 11 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> ((((proj` F) o. (proj` G)) o. (proj` H))` y) = ((proj` ((F i^i G) i^i H))` y))
17	16	opreq2d 3976	. . . . . . . . . 10 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H))) -> (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)) = (x .ih ((proj` ((F i^i G) i^i H))` y)))
18	17	ad2antlr 405	. . . . . . . . 9 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)) = (x .ih ((proj` ((F i^i G) i^i H))` y)))
19	11, 15, 18	3eqtr4d 1517	. . . . . . . 8 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) .ih y) = (x .ih ((((proj` F) o. (proj` G)) o. (proj` H))` y)))
20	8, 5, 6	pjadj2co 10132	. . . . . . . . 9 |- ((x e. H~ /\ y e. H~) -> (((((proj` H) o. (proj` F)) o. (proj` G))` x) .ih y) = (x .ih ((((proj` G) o. (proj` F)) o. (proj` H))` y)))
21	20	adantlr 393	. . . . . . . 8 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (((((proj` H) o. (proj` F)) o. (proj` G))` x) .ih y) = (x .ih ((((proj` G) o. (proj` F)) o. (proj` H))` y)))
22	4, 19, 21	3eqtr4d 1517	. . . . . . 7 |- (((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ (((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` G) o. (proj` F)) o. (proj` H)))) /\ y e. H~) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) .ih y) = ((