Theorem pj3s 5659

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	. . . . . . . . 9 |- F e. CH
2		pjadj2co.2	. . . . . . . . 9 |- G e. CH
3	1, 2	chincl 5382	. . . . . . . 8 |- (F i^i G) e. CH
4		pjadj2co.3	. . . . . . . 8 |- H e. CH
5	3, 4	chincl 5382	. . . . . . 7 |- ((F i^i G) i^i H) e. CH
6	5	pjv 5589	. . . . . 6 |- ((((((Proj` F) o. (Proj` G)) o. (Proj` H))` x) e. ((F i^i G) i^i H) /\ (x -v ((((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) +v (x -v ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x)))) = ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x))
7	1, 2, 4	pj2cocl 5657	. . . . . . . . . . . 12 |- (x e. H~ -> ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x) e. F)
8	7	adantl 305	. . . . . . . . . . 11 |- ((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 1502	. . . . . . . . . . . . 13 |- (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 5588	. . . . . . . . . . . . . . . 16 |- (Proj` F):H~-->H~
11	2	pjf 5588	. . . . . . . . . . . . . . . 16 |- (Proj` G):H~-->H~
12	10, 11	hocof 5600	. . . . . . . . . . . . . . 15 |- ((Proj` F) o. (Proj` G)):H~-->H~
13	4	pjf 5588	. . . . . . . . . . . . . . 15 |- (Proj` H):H~-->H~
14	12, 13	hocofn 5601	. . . . . . . . . . . . . 14 |- (((Proj` F) o. (Proj` G)) o. (Proj` H)) Fn H~
15		fnfvrn 2889	. . . . . . . . . . . . . 14 |- (((((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 518	. . . . . . . . . . . . 13 |- (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 22	. . . . . . . . . . . 12 |- (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 277	. . . . . . . . . . 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)
19	8, 18	jca 236	. . . . . . . . . 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 /\ ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x) e. G))
20		elin 1635	. . . . . . . . . 10 |- (((((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 175	. . . . . . . . 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 i^i G))
22	21	adantll 309	. . . . . . . 8 |- ((((((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 2831	. . . . . . . . . . . 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))` x) = ((((Proj` H) o. (Proj` G)) o. (Proj` F))` x))
24	23	eleq1d 1155	. . . . . . . . . . 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) e. H <-> ((((Proj` H) o. (Proj` G)) o. (Proj` F))` x) e. H))
25	4, 2, 1	pj2cocl 5657	. . . . . . . . . . 11 |- (x e. H~ -> ((((Proj` H) o. (Proj` G)) o. (Proj` F))` x) e. H)
26	24, 25	syl5bir 184	. . . . . . . . . 10 |- ((((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 277	. . . . . . . . 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)
28	27	adantlr 310	. . . . . . . 8 |- ((((((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 236	. . . . . . 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) /\ ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x) e. H))
30		elin 1635	. . . . . . 7 |- (((((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 175	. . . . . 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) i^i H))
32	12, 13	hococl 5599	. . . . . . . . . 10 |- (x e. H~ -> ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x) e. H~)
33		hvsubclt 4998	. . . . . . . . . 10 |- ((x e. H~ /\ ((((Proj` F) o. (Proj` G)) o. (Proj` H))` x)