Theorem pjss2co 5634

Description: Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112.

Hypotheses

Ref	Expression
pjco.1	|- G e. CH
pjco.2	|- H e. CH

Assertion

Ref	Expression
pjss2co	|- (G (_ H <-> ((Proj` G) o. (Proj` H)) = (Proj` G))

Proof of Theorem pjss2co

Step	Hyp	Ref	Expression
1		pjco.1	. . . . . . . 8 |- G e. CH
2		pjco.2	. . . . . . . 8 |- H e. CH
3	1, 2	pjco 5628	. . . . . . 7 |- (x e. H~ -> (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` ((Proj` H)` x)))
4	3	adantl 305	. . . . . 6 |- ((G (_ H /\ x e. H~) -> (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` ((Proj` H)` x)))
5		fveq2 2832	. . . . . . . . . . . 12 |- (x = if(x e. H~, x, 0v) -> ((Proj` H)` x) = ((Proj` H)` if(x e. H~, x, 0v)))
6	5	fveq2d 2836	. . . . . . . . . . 11 |- (x = if(x e. H~, x, 0v) -> ((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` ((Proj` H)` if(x e. H~, x, 0v))))
7		fveq2 2832	. . . . . . . . . . 11 |- (x = if(x e. H~, x, 0v) -> ((Proj` G)` x) = ((Proj` G)` if(x e. H~, x, 0v)))
8	6, 7	cleq12d 1115	. . . . . . . . . 10 |- (x = if(x e. H~, x, 0v) -> (((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` x) <-> ((Proj` G)` ((Proj` H)` if(x e. H~, x, 0v))) = ((Proj` G)` if(x e. H~, x, 0v))))
9	8	imbi2d 464	. . . . . . . . 9 |- (x = if(x e. H~, x, 0v) -> ((G (_ H -> ((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` x)) <-> (G (_ H -> ((Proj` G)` ((Proj` H)` if(x e. H~, x, 0v))) = ((Proj` G)` if(x e. H~, x, 0v)))))
10		ax-hvzercl 4987	. . . . . . . . . . 11 |- 0v e. H~
11	10	elimel 1793	. . . . . . . . . 10 |- if(x e. H~, x, 0v) e. H~
12	1, 11, 2	pjss2 5571	. . . . . . . . 9 |- (G (_ H -> ((Proj` G)` ((Proj` H)` if(x e. H~, x, 0v))) = ((Proj` G)` if(x e. H~, x, 0v)))
13	9, 12	dedth 1784	. . . . . . . 8 |- (x e. H~ -> (G (_ H -> ((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` x)))
14	13	com12 13	. . . . . . 7 |- (G (_ H -> (x e. H~ -> ((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` x)))
15	14	imp 277	. . . . . 6 |- ((G (_ H /\ x e. H~) -> ((Proj` G)` ((Proj` H)` x)) = ((Proj` G)` x))
16	4, 15	eqtrd 1128	. . . . 5 |- ((G (_ H /\ x e. H~) -> (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` x))
17	16	exp 291	. . . 4 |- (G (_ H -> (x e. H~ -> (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` x)))
18	17	r19.21aiv 1259	. . 3 |- (G (_ H -> A.x e. H~ (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` x))
19	1	pjf 5588	. . . . 5 |- (Proj` G):H~-->H~
20	2	pjf 5588	. . . . 5 |- (Proj` H):H~-->H~
21	19, 20	hocof 5600	. . . 4 |- ((Proj` G) o. (Proj` H)):H~-->H~
22	21, 19	hoeq 5595	. . 3 |- (A.x e. H~ (((Proj` G) o. (Proj` H))` x) = ((Proj` G)` x) <-> ((Proj` G) o. (Proj` H)) = (Proj` G))
23	18, 22	sylib 173	. 2 |- (G (_ H -> ((Proj` G) o. (Proj` H)) = (Proj` G))
24		fveq1 2831	. . . . . . . . . . . 12 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> (((Proj` G) o. (Proj` H))` y) = ((Proj` G)` y))
25	24	opreq2d 3013	. . . . . . . . . . 11 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> (x .i (((Proj` G) o. (Proj` H))` y)) = (x .i ((Proj` G)` y)))
26	25	ad2antlr 321	. . . . . . . . . 10 |- (((x e. H~ /\ ((Proj` G) o. (Proj` H)) = (Proj` G)) /\ y e. H~) -> (x .i (((Proj` G) o. (Proj` H))` y)) = (x .i ((Proj` G)` y)))
27	2, 1	pjadjco 5631	. . . . . . . . . . 11 |- ((x e. H~ /\ y e. H~) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (x .i (((Proj` G) o. (Proj` H))` y)))
28	27	adantlr 310	. . . . . . . . . 10 |- (((x e. H~ /\ ((Proj` G) o. (Proj` H)) = (Proj` G)) /\ y e. H~) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (x .i (((Proj` G) o. (Proj` H))` y)))
29	1	pjadjt 5576	. . . . . . . . . . 11 |- ((x e. H~ /\ y e. H~) -> (((Proj` G)` x) .i y) = (x .i ((Proj` G)` y)))
30	29	adantlr 310	. . . . . . . . . 10 |- (((x e. H~ /\ ((Proj` G) o. (Proj` H)) = (Proj` G)) /\ y e. H~) -> (((Proj` G)` x) .i y) = (x .i ((Proj` G)` y)))
31	26, 28, 30	3eqtr4d 1134	. . . . . . . . 9 |- (((x e. H~ /\ ((Proj` G) o. (Proj` H)) = (Proj` G)) /\ y e. H~) -> ((((Proj` H) o. (Proj` G))` x) .i y) = (((Proj` G)` x) .i y))
32	31	exp31 293	. . . . . . . 8 |- (x e. H~ -> (((Proj` G) o. (Proj` H)) = (Proj` G) -> (y e. H~ -> ((((Proj` H) o. (Proj` G))` x) .i y) = (((Proj` G)` x) .i y))))
33	32	r19.21adv 1262	. . . . . . 7 |- (x e. H~ -> (((Proj` G) o. (Proj` H)) = (Proj` G) -> A.y e. H~ ((((Proj` H) o. (Proj` G))` x) .i y) = (((Proj` G)` x) .i y)))
34		hial2eqt 5060	. . . . . . . 8 |- (((((Proj` H) o. (Proj` G))` x) e. H~ /\ ((Proj` G)` x) e. H~) -> (A.y e. H~ ((((Proj` H) o. (Proj` G))` x) .i y) = (((Proj` G)` x) .i y) <-> (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x)))
35	2, 1	pjcohcl 5630	. . . . . . . 8 |- (x e. H~ -> (((Proj` H) o. (Proj` G))` x) e. H~)
36	1	pjhcl 5256	. . . . . . . 8 |- (x e. H~ -> ((Proj` G)` x) e. H~)
37	34, 35, 36	sylanc 361	. . . . . . 7 |- (x e. H~ -> (A.y e. H~ ((((Proj` H) o. (Proj` G))` x) .i y) = (((Proj` G)` x) .i y) <-> (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x)))
38	33, 37	sylibd 177	. . . . . 6 |- (x e. H~ -> (((Proj` G) o. (Proj` H)) = (Proj` G) -> (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x)))
39	38	com12 13	. . . . 5 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> (x e. H~ -> (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x)))
40	39	r19.21aiv 1259	. . . 4 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> A.x e. H~ (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x))
41	20, 19	hocof 5600	. . . . 5 |- ((Proj` H) o. (Proj` G)):H~-->H~
42	41, 19	hoeq 5595	. . . 4 |- (A.x e. H~ (((Proj` H) o. (Proj` G))` x) = ((Proj` G)` x) <-> ((Proj` H) o. (Proj` G)) = (Proj` G))
43	40, 42	sylib 173	. . 3 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> ((Proj` H) o. (Proj` G)) = (Proj` G))
44	1, 2	pjss1co 5633	. . 3 |- (G (_ H <-> ((Proj` H) o. (Proj` G)) = (Proj` G))
45	43, 44	sylibr 175	. 2 |- (((Proj` G) o. (Proj` H)) = (Proj` G) -> G (_ H)
46	23, 45	impbi 139	1 |- (G (_ H <-> ((Proj` G) o. (Proj` H)) = (Proj` G))

Syntax hints: