Theorem pj3s 10091

Description: Stronger projection triplet theorem.

Hypotheses

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

Assertion

Ref	Expression
pj3s	|- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) -> (((proj` F) o. (proj` G)) o. (proj` H)) = (proj` ((F i^i G) i^i H)))

Proof of Theorem pj3s

Step	Hyp	Ref	Expression
1		pjadj2co.1	. . . . . . . 8 |- F e. CH
2		pjadj2co.2	. . . . . . . 8 |- G e. CH
3	1, 2	chincl 9338	. . . . . . 7 |- (F i^i G) e. CH
4		pjadj2co.3	. . . . . . 7 |- H e. CH
5	3, 4	chincl 9338	. . . . . 6 |- ((F i^i G) i^i H) e. CH
6	5	pjv 9607	. . . . 5 |- ((((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ((F i^i G) i^i H) /\ (x -h ((((proj` F) o. (proj` G)) o. (proj` H))` x)) e. (_|_` ((F i^i G) i^i H))) -> ((proj` ((F i^i G) i^i H))` (((((proj` F) o. (proj` G)) o. (proj` H))` x) +h (x -h ((((proj` F) o. (proj` G)) o. (proj` H))` x)))) = ((((proj` F) o. (proj` G)) o. (proj` H))` x))
7	1, 2, 4	pj2cocl 10089	. . . . . . . . . . 11 |- (x e. H~ -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. F)
8	7	adantl 388	. . . . . . . . . 10 |- ((ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. F)
9		ssel 2060	. . . . . . . . . . . 12 |- (ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ran (((proj` F) o. (proj` G)) o. (proj` H)) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. G))
10	1	pjf 9606	. . . . . . . . . . . . . . 15 |- (proj` F):H~-->H~
11	2	pjf 9606	. . . . . . . . . . . . . . 15 |- (proj` G):H~-->H~
12	10, 11	hocof 9649	. . . . . . . . . . . . . 14 |- ((proj` F) o. (proj` G)):H~-->H~
13	4	pjf 9606	. . . . . . . . . . . . . 14 |- (proj` H):H~-->H~
14	12, 13	hocofn 9650	. . . . . . . . . . . . 13 |- (((proj` F) o. (proj` G)) o. (proj` H)) Fn H~
15		fnfvelrn 3808	. . . . . . . . . . . . 13 |- (((((proj` F) o. (proj` G)) o. (proj` H)) Fn H~ /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ran (((proj` F) o. (proj` G)) o. (proj` H)))
16	14, 15	mpan 694	. . . . . . . . . . . 12 |- (x e. H~ -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ran (((proj` F) o. (proj` G)) o. (proj` H)))
17	9, 16	syl5 21	. . . . . . . . . . 11 |- (ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G -> (x e. H~ -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. G))
18	17	imp 350	. . . . . . . . . 10 |- ((ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. G)
19	8, 18	jca 288	. . . . . . . . 9 |- ((ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G /\ x e. H~) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. F /\ ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. G))
20		elin 2204	. . . . . . . . 9 |- (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. (F i^i G) <-> (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. F /\ ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. G))
21	19, 20	sylibr 200	. . . . . . . 8 |- ((ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. (F i^i G))
22	21	adantll 392	. . . . . . 7 |- ((((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. (F i^i G))
23		fveq1 3718	. . . . . . . . . . 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))` x) = ((((proj` H) o. (proj` G)) o. (proj` F))` x))
24	23	eleq1d 1538	. . . . . . . . . 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))` x) e. H <-> ((((proj` H) o. (proj` G)) o. (proj` F))` x) e. H))
25	4, 2, 1	pj2cocl 10089	. . . . . . . . . 10 |- (x e. H~ -> ((((proj` H) o. (proj` G)) o. (proj` F))` x) e. H)
26	24, 25	syl5bir 210	. . . . . . . . 9 |- ((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) -> (x e. H~ -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H))
27	26	imp 350	. . . . . . . 8 |- (((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H)
28	27	adantlr 393	. . . . . . 7 |- ((((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H)
29	22, 28	jca 288	. . . . . 6 |- ((((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) /\ x e. H~) -> (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. (F i^i G) /\ ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H))
30		elin 2204	. . . . . 6 |- (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ((F i^i G) i^i H) <-> (((((proj` F) o. (proj` G)) o. (proj` H))` x) e. (F i^i G) /\ ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H))
31	29, 30	sylibr 200	. . . . 5 |- ((((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) /\ x e. H~) -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. ((F i^i G) i^i H))
32	12, 13	hococl 9648	. . . . . . . . 9 |- (x e. H~ -> ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H~)
33		hvsubclt 8842	. . . . . . . . 9 |- ((x e. H~ /\ ((((proj` F) o. (proj` G)) o. (proj` H))` x) e. H~) -> (x -h ((((proj` F) o. (proj` G)) o. (proj` H))` x)) e. H~)
34	32, 33	mpdan 703	. . . . . . . 8 |- (x e. H~ -> (x -h ((((proj` F) o. (proj` G)) o. (proj` H))` x)) e. H~)
35	34	adantl 388	. . . . . . 7 |- ((((((proj` F) o. (proj` G)) o. (proj` H)) = (((proj` H) o. (proj` G)) o. (proj` F)) /\ ran (((proj` F) o. (proj` G)) o. (proj` H)) (_ G) /\ x e. H~) -> (x -h ((((proj` F) o. (proj` G)) o. (proj` H))` x)) e. H~)
36		pm3.26 319	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e.