Theorem pjssm 9543

Description: Projection meet property. Remark in [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) -h ((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 9168	. . . . . . 7 |- ((proj` H)` A) e. H
4		ssel 2053	. . . . . . 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 9168	. . . . . 6 |- ((proj` G)` A) e. G
8	5, 7	jctil 292	. . . . 5 |- (H (_ G -> (((proj` G)` A) e. G /\ ((proj` H)` A) e. G))
9	6	chshi 9018	. . . . . 6 |- G e. SH
10		shsubcltOLD 9011	. . . . . 6 |- (G e. SH -> ((((proj` G)` A) e. G /\ ((proj` H)` A) e. G) -> (((proj` G)` A) -h ((proj` H)` A)) e. G))
11	9, 10	ax-mp 7	. . . . 5 |- ((((proj` G)` A) e. G /\ ((proj` H)` A) e. G) -> (((proj` G)` A) -h ((proj` H)` A)) e. G)
12	8, 11	syl 10	. . . 4 |- (H (_ G -> (((proj` G)` A) -h ((proj` H)` A)) e. G)
13	1, 6	chsscon3 9299	. . . . . 6 |- (H (_ G <-> (_|_` G) (_ (_|_` H))
14	6	choccl 9101	. . . . . . . . . 10 |- (_|_` G) e. CH
15	14, 2	pjcli 9168	. . . . . . . . 9 |- ((proj` (_|_` G))` A) e. (_|_` G)
16		ssel 2053	. . . . . . . . 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	choccl 9101	. . . . . . . . 9 |- (_|_` H) e. CH
19	18, 2	pjcli 9168	. . . . . . . 8 |- ((proj` (_|_` H))` A) e. (_|_` H)
20	17, 19	jctil 292	. . . . . . 7 |- ((_|_` G) (_ (_|_` H) -> (((proj` (_|_` H))` A) e. (_|_` H) /\ ((proj` (_|_` G))` A) e. (_|_` H)))
21	18	chshi 9018	. . . . . . . 8 |- (_|_` H) e. SH
22		shsubcltOLD 9011	. . . . . . . 8 |- ((_|_` H) e. SH -> ((((proj` (_|_` H))` A) e. (_|_` H) /\ ((proj` (_|_` G))` A) e. (_|_` H)) -> (((proj` (_|_` H))` A) -h ((proj` (_|_` G))` A)) e. (_|_` H)))
23	21, 22	ax-mp 7	. . . . . . 7 |- ((((proj` (_|_` H))` A) e. (_|_` H) /\ ((proj` (_|_` G))` A) e. (_|_` H)) -> (((proj` (_|_` H))` A) -h ((proj` (_|_` G))` A)) e. (_|_` H))
24	20, 23	syl 10	. . . . . 6 |- ((_|_` G) (_ (_|_` H) -> (((proj` (_|_` H))` A) -h ((proj` (_|_` G))` A)) e. (_|_` H))
25	13, 24	sylbi 199	. . . . 5 |- (H (_ G -> (((proj` (_|_` H))` A) -h ((proj` (_|_` G))` A)) e. (_|_` H))
26	1, 2, 6	pjsslem 9541	. . . . 5 |- (((proj` (_|_` H))` A) -h ((proj` (_|_` G))` A)) = (((proj` G)` A) -h ((proj` H)` A))
27	25, 26	syl5eqelr 1545	. . . 4 |- (H (_ G -> (((proj` G)` A) -h ((proj` H)` A)) e. (_|_` H))
28	12, 27	jca 288	. . 3 |- (H (_ G -> ((((proj` G)` A) -h ((proj` H)` A)) e. G /\ (((proj` G)` A) -h ((proj` H)` A)) e. (_|_` H)))
29		elin 2197	. . . 4 |- ((((proj` G)` A) -h ((proj` H)` A)) e. (G i^i (_|_` H)) <-> ((((proj` G)` A) -h ((proj` H)` A)) e. G /\ (((proj` G)` A) -h ((proj` H)` A)) e. (_|_` H)))
30	6, 18	chincl 9298	. . . . 5 |- (G i^i (_|_` H)) e. CH
31	6, 2	pjhcli 9169	. . . . . 6 |- ((proj` G)` A) e. H~
32	1, 2	pjhcli 9169	. . . . . 6 |- ((proj` H)` A) e. H~
33	31, 32	hvsubcl 8812	. . . . 5 |- (((proj` G)` A) -h ((proj` H)` A)) e. H~
34	30, 33	pjch 9180	. . . 4 |- ((((proj` G)` A) -h ((proj` H)` A)) e. (G i^i (_|_` H)) <-> ((proj` (G i^i (_|_` H)))` (((proj` G)` A) -h ((proj` H)` A))) = (((proj` G)` A) -h ((proj` H)` A)))
35	29, 34	bitr3 175	. . 3 |- (((((proj` G)` A) -h ((proj` H)` A)) e. G /\ (((proj` G)` A) -h ((proj` H)` A)) e. (_|_` H)) <-> ((proj` (G i^i (_|_` H)))` (((proj` G)` A) -h ((proj` H)` A))) = (((proj` G)` A) -h ((proj` H)` A)))
36	28, 35	sylib 198	. 2 |- (H (_ G -> ((proj` (G i^i (_|_` H)))` (((proj` G)` A) -h ((proj` H)` A))) = (((proj` G)` A) -h ((proj` H)` A)))
37	30, 31, 32	pjsub 9540	. . 3 |- ((proj` (G i^i (_|_` H)))` (((proj` G)` A) -h ((proj` H)` A))) = (((proj` (G i^i (_|_` H)))` ((proj` G)` A)) -h ((proj` (G i^i (_|_` H)))` ((proj` H)` A)))
38	30, 31	pjhcli 9169	. . . 4 |- ((proj` (G i^i (_|_` H)))` ((proj` G)` A)) e. H~
39	30, 32	pjhcli 9169	. . . 4 |- ((proj` (G i^i (_|_` H)))` ((proj` H)` A)) e. H~
40	38, 39	hvsubval 8811	. . 3 |- (((proj` (G i^i (_|_` H)))` ((proj` G)` A)) -h ((proj` (G i^i (_|_` H)))` ((proj` H)` A))) = (((proj` (G i^i (_|_` H)))` ((proj` G)` A)) +h (-u1 .h ((proj` (G i^i (_|_` H)))` ((proj` H)` A))))
41		inss1 2220	. . . . . 6 |- (G i^i (_|_` H)) (_ G
42	30, 2, 6	pjss2 9542	. . . . . 6 |- ((G i^i (_|_` H)) (_ G -> ((proj` (G i^i (_|_` H)))` ((proj` G)` A)) = ((proj` (G i^i (_|_` H)))` A))
43	41, 42	ax-mp 7	. . . . 5 |- ((proj` (G i^i (_|_` H)))` ((proj` G)` A)) = ((proj` (G i^i (_|_` H)))` A)
44	1	chshi 9018	. . . . . . . . . . 11 |- H e. SH
45		shococss 9083	. . . . . . . . . . 11 |- (H e. SH -> H (_ (_|_` (_|_` H)))
46	44, 45	ax-mp 7	. . . . . . . . . 10 |- H (_ (_|_` (_|_` H))
47		inss2 2221	. . . . . . . . . . 11 |- (G i^i (_|_` H)) (_ (_|_` H)
48	30, 18	chsscon3 9299	. . . . . . . . . . 11 |- ((G i^i (_|_` H)) (_ (_|_` H) <-> (_|_` (_|_` H)) (_ (_|_` (G i^i (_|_` H))))
49	47, 48	mpbi 189	. . . . . . . . . 10 |- (_|_` (_|_` H)) (_ (_|_` (G i^i (_|_` H)))
50	46, 49	sstri 2063	. . . . . . . . 9 |- H (_ (_|_` (G i^i (_|_` H)))
51	50, 3	sselii 2056	. . . . . . . 8 |- ((proj` H)` A) e. (_|_` (G i^i (_|_` H)))
52	30, 32	pjoc2 9186	. . . . . . . 8 |- (((proj` H)` A) e. (_|_` (G i^i (_|_` H))) <-> ((proj` (G i^i (_|_` H)))` ((proj` H)` A)) = 0h)
53	51, 52	mpbi 189	. . . . . . 7 |- ((proj` (G i^i (_|_` H)))` ((proj` H)` A)) = 0h
54	53	opreq2i 3957	. . . . . 6 |- (-u1 .h ((proj` (G i^i (_|_` H)))` ((proj` H)` A))) = (-u1 .h 0h)
55		ax1cn 5241	. . . . . . . 8 |- 1 e. CC
56	55	negcl 5341	. . . . . . 7 |- -u1 e. CC
57		hvmul0t 8814	. . . . . . 7 |- (-u1 e. CC -> (-u1 .h 0h) = 0h)
58	56, 57	ax-mp 7	. . . . . 6 |- (-u1 .h 0h) = 0h
59	54, 58	eqtr 1487	. . . . 5 |- (-u1 .h ((proj` (G i^i (_|_` H)))` ((proj` H)` A))) = 0h
60	43, 59	opreq12i 3958	. . . 4 |- (((proj` (G i^i (_|_` H)