Theorem pj3cor1 5661

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 2831	. . . . . . . . . . 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 3013	. . . . . . . . . 10 |- ((((Proj` F) o. (Proj` G)) o. (Proj` H)) = (((Proj` G) o. (Proj` F)) o. (Proj` H)) -> (x .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)) = (x .i ((((Proj` G) o. (Proj` F)) o. (Proj` H))` y)))
3	2	adantl 305	. . . . . . . . 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 .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)) = (x .i ((((Proj` G) o. (Proj` F)) o. (Proj` H))` y)))
4	3	ad2antlr 321	. . . . . . . 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 .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)) = (x .i ((((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 5382	. . . . . . . . . . . 12 |- (F i^i G) e. CH
8		pjadj2co.3	. . . . . . . . . . . 12 |- H e. CH
9	7, 8	chincl 5382	. . . . . . . . . . 11 |- ((F i^i G) i^i H) e. CH
10	9	pjadjt 5576	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (((Proj` ((F i^i G) i^i H))` x) .i y) = (x .i ((Proj` ((F i^i G) i^i H))` y)))
11	10	adantlr 310	. . . . . . . . 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) .i y) = (x .i ((Proj` ((F i^i G) i^i H))` y)))
12	5, 6, 8	pj3 5660	. . . . . . . . . . . 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 2834	. . . . . . . . . . 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 3012	. . . . . . . . . 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) .i y) = (((Proj` ((F i^i G) i^i H))` x) .i y))
15	14	ad2antlr 321	. . . . . . . . 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) .i y) = (((Proj` ((F i^i G) i^i H))` x) .i y))
16	12	fveq1d 2834	. . . . . . . . . . 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 3013	. . . . . . . . . 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 .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)) = (x .i ((Proj` ((F i^i G) i^i H))` y)))
18	17	ad2antlr 321	. . . . . . . . 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 .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)) = (x .i ((Proj` ((F i^i G) i^i H))` y)))
19	11, 15, 18	3eqtr4d 1134	. . . . . . . 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) .i y) = (x .i ((((Proj` F) o. (Proj` G)) o. (Proj` H))` y)))
20	8, 5, 6	pjadj2co 5656	. . . . . . . . 9 |- ((x e. H~ /\ y e. H~) -> (((((Proj` H) o. (Proj` F)) o. (Proj` G))` x) .i y) = (x .i ((((Proj` G) o. (Proj` F)) o. (Proj` H))` y)))
21	20	adantlr 310	. . . . . . . 8 |- (((x e. H~ /\ ((((Proj` F) o. (Proj` G)) o. (Proj` H)) = (((Proj` H) o. (Proj` G)) o. (Proj` F)) /\ (((Proj` F