Theorem pjssm 5572

Description: Projection meet property. Remark of [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112.

Hypotheses

Ref	Expression
pjidm.1	|- H e. CH
pjidm.2	|- A e. H~
pjsslem.1	|- G e. CH

Assertion

Ref	Expression
pjssm	|- (H (_ G -> (((Proj` G)` A) -v ((Proj` H)` A)) = ((Proj` (G i^i (_|_` H)))` A))

Proof of Theorem pjssm

Step	Hyp	Ref	Expression
1		pjidm.1	. . . . . . . 8 |- H e. CH
2		pjidm.2	. . . . . . . 8 |- A e. H~
3	1, 2	pjcli 5257	. . . . . . 7 |- ((Proj` H)` A) e. H
4		ssel 1502	. . . . . . 7 |- (H (_ G -> (((Proj` H)` A) e. H -> ((Proj` H)` A) e. G))
5	3, 4	mpi 44	. . . . . 6 |- (H (_ G -> ((Proj` H)` A) e. G)
6		pjsslem.1	. . . . . . 7 |- G e. CH
7	6, 2	pjcli 5257	. . . . . 6 |- ((Proj` G)` A) e. G
8	5, 7	jctil 240	. . . . 5 |- (H (_ G -> (((Proj` G)` A) e. G /\ ((Proj` H)` A) e. G))
9	6	chshi 5132	. . . . . 6 |- G e. SH
10		shsubclt 5125	. . . . . 6 |- (G e. SH -> ((((Proj` G)` A) e. G /\ ((Proj` H)` A) e. G) -> (((Proj` G)` A) -v ((Proj` H)` A)) e. G))
11	9, 10	ax-mp 6	. . . . 5 |- ((((Proj` G)` A) e. G /\ ((Proj` H)` A) e. G) -> (((Proj` G)` A) -v ((Proj` H)` A)) e. G)
12	8, 11	syl 12	. . . 4 |- (H (_ G -> (((Proj` G)` A) -v ((Proj` H)` A)) e. G)
13	1, 6	chsscon3 5383	. . . . . 6 |- (H (_ G <-> (_|_` G) (_ (_|_` H))
14	6	chocl 5192	. . . . . . . . . 10 |- (_|_` G) e. CH
15	14, 2	pjcli 5257	. . . . . . . . 9 |- ((Proj` (_|_` G))` A) e. (_|_` G)
16		ssel 1502	. . . . . . . . 9 |- ((_|_` G) (_ (_|_` H) -> (((Proj` (_|_` G))` A) e. (_|_` G) -> ((Proj` (_|_` G))` A) e. (_|_` H)))
17	15, 16	mpi 44	. . . . . . . 8 |- ((_|_` G) (_ (_|_` H) -> ((Proj` (_|_` G))` A) e. (_|_` H))
18	1	chocl 5192	. . . . . . . . 9 |- (_|_` H) e. CH
19	18, 2	pjcli 5257	. . . . . . . 8 |- ((Proj` (_|_` H))` A) e. (_|_` H)
20	17, 19	jctil 240	. . . . . . 7 |- ((_|_` G) (_ (_|_` H) -> (((Proj` (_|_` H))` A) e. (_|_` H) /\ ((Proj` (_|_` G))` A) e. (_|_` H)))
21	18	chshi 5132	. . . . . . . 8 |- (_|_` H) e. SH
22		shsubclt 5125	. . . . . . . 8 |- ((_|_` H) e. SH -> ((((Proj` (_|_` H))` A) e. (_|_` H) /\ ((Proj` (_|_` G))` A) e. (_|_` H)) -> (((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) e. (_|_` H)))
23	21, 22	ax-mp 6	. . . . . . 7 |- ((((Proj` (_|_` H))` A) e. (_|_` H) /\ ((Proj` (_|_` G))` A) e. (_|_` H)) -> (((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) e. (_|_` H))
24	20, 23	syl 12	. . . . . 6 |- ((_|_` G) (_ (_|_` H) -> (((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) e. (_|_` H))
25	13, 24	sylbi 174	. . . . 5 |- (H (_ G -> (((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) e. (_|_` H))
26	1, 2, 6	pjsslem 5570	. . . . . 6 |- (((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) = (((Proj` G)` A) -v ((Proj` H)` A))
27	26	eleq1i 1152	. . . . 5 |- ((((Proj` (_|_` H))` A) -v ((Proj` (_|_` G))` A)) e. (_|_` H) <-> (((Proj` G)` A) -v ((Proj` H)` A)) e. (_|_` H))
28	25, 27	sylib 173	. . . 4 |- (H (_ G -> (((Proj` G)` A) -v ((Proj` H)` A)) e. (_|_` H))
29	12, 28	jca 236	. . 3 |- (H (_ G -> ((((Proj` G)` A) -v ((Proj` H)` A)) e. G /\ (((Proj` G)` A) -v ((Proj` H)` A)) e. (_|_` H)))
30		elin 1635	. . . 4 |- ((((Proj` G)` A) -v ((Proj` H)` A)) e. (G i^i (_|_` H)) <-> ((((Proj` G)` A) -v ((Proj` H)` A)) e. G /\ (((Proj` G)` A) -v ((Proj` H)` A)) e. (_|_` H)))
31	6, 18	chincl 5382	. . . . 5 |- (G i^i (_|_` H)) e. CH
32	6, 2	pjhcli 5258	. . . . . 6 |- ((Proj` G)` A) e. H~
33	1, 2	pjhcli 5258	. . . . . 6 |- ((Proj` H)` A) e. H~
34	32, 33	hvsubcl 5002	. . . . 5 |- (((Proj` G)` A) -v ((Proj` H)` A)) e. H~
35	31, 34	pjch 5269	. . . 4 |- ((((Proj` G)` A) -v ((Proj` H)` A)) e. (G i^i (_|_` H)) <-> ((Proj` (G i^i (_|_` H)))` (((Proj` G)` A) -v ((Proj` H)` A))) = (((Proj` G)` A) -v ((Proj` H)` A)))
36	30, 35	bitr3 153	. . 3 |- (((((Proj` G)` A) -v ((Proj` H)` A)) e. G /\ (((Proj` G)` A) -v ((Proj` H)` A)) e. (_|_` H)) <-> ((Proj` (G i^i (_|_` H)))` (((Proj` G)` A) -v ((Proj` H)` A))) = (((Proj` G)` A) -v ((Proj` H)` A)))
37	29, 36	sylib 173	. 2 |- (H (_ G -> ((Proj` (G i^i (_|_` H)))` (((Proj` G)` A) -v ((Proj` H)` A))) = (((Proj` G)` A) -v ((Proj` H)` A)))
38	31, 32, 33	pjsub 5569	. . 3 |- ((Proj` (G i^i (_|_` H)))` (((Proj` G)` A) -v ((Proj` H)` A))) = (((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) -v ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A)))
39	31, 32	pjhcli 5258	. . . 4 |- ((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) e. H~
40	31, 33	pjhcli 5258	. . . 4 |- ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A)) e. H~
41	39, 40	hvsubval 5001	. . 3 |- (((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) -v ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A))) = (((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) +v (-u1 .s ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A))))
42		inss1 1657	. . . . . 6 |- (G i^i (_|_` H)) (_ G
43	31, 2, 6	pjss2 5571	. . . . . 6 |- ((G i^i (_|_` H)) (_ G -> ((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) = ((Proj` (G i^i (_|_` H)))` A))
44	42, 43	ax-mp 6	. . . . 5 |- ((Proj` (G i^i (_|_` H)))` ((Proj` G)` A)) = ((Proj` (G i^i (_|_` H)))` A)
45	1	chshi 5132	. . . . . . . . . . 11 |- H e. SH
46		shococss 5175	. . . . . . . . . . 11 |- (H e. SH -> H (_ (_|_` (_|_` H)))
47	45, 46	ax-mp 6	. . . . . . . . . 10 |- H (_ (_|_` (_|_` H))
48		inss2 1658	. . . . . . . . . . 11 |- (G i^i (_|_` H)) (_ (_|_` H)
49	31, 18	chsscon3 5383	. . . . . . . . . . 11 |- ((G i^i (_|_` H)) (_ (_|_` H) <-> (_|_` (_|_` H)) (_ (_|_` (G i^i (_|_` H))))
50	48, 49	mpbi 164	. . . . . . . . . 10 |- (_|_` (_|_` H)) (_ (_|_` (G i^i (_|_` H)))
51	47, 50	sstri 1512	. . . . . . . . 9 |- H (_ (_|_` (G i^i (_|_` H)))
52	51, 3	sselii 1505	. . . . . . . 8 |- ((Proj` H)` A) e. (_|_` (G i^i (_|_` H)))
53	31, 33	pjoc2 5273	. . . . . . . 8 |- (((Proj` H)` A) e. (_|_` (G i^i (_|_` H))) <-> ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A)) = 0v)
54	52, 53	mpbi 164	. . . . . . 7 |- ((Proj` (G i^i (_|_` H)))` ((Proj` H)` A)) = 0v
55	54	opreq2i 3010	. . . . . 6 |- (-u1 .s ((Proj` (G i^i (_|_` H)))` (