Theorem sumdmdi 5785

Description: If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark of [MaedaMaeda] p. 139.

Hypotheses

Ref	Expression
sumdmdi.1	|- A e. CH
sumdmdi.2	|- B e. CH

Assertion

Ref	Expression
sumdmdi	|- ((A +H B) = (A vH B) -> (_|_` A) MH (_|_` B))

Proof of Theorem sumdmdi

Step	Hyp	Ref	Expression
1		ineq2 1639	. . . . . . 7 |- ((A +H B) = (A vH B) -> (x i^i (A +H B)) = (x i^i (A vH B)))
2	1	adantr 306	. . . . . 6 |- (((A +H B) = (A vH B) /\ (x e. CH /\ B (_ x)) -> (x i^i (A +H B)) = (x i^i (A vH B)))
3		chsh 5131	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. CH -> x e. SH)
4		shsubclt 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. SH -> ((y e. x /\ w e. x) -> (y -v w) e. x))
5	4	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. SH -> (y e. x -> (w e. x -> (y -v w) e. x)))
6	3, 5	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. CH -> (y e. x -> (w e. x -> (y -v w) e. x)))
7		ssel2 1503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B (_ x /\ w e. B) -> w e. x)
8	6, 7	syl7 24	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. CH -> (y e. x -> ((B (_ x /\ w e. B) -> (y -v w) e. x)))
9	8	exp4a 295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. CH -> (y e. x -> (B (_ x -> (w e. B -> (y -v w) e. x))))
10	9	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. CH -> (B (_ x -> (y e. x -> (w e. B -> (y -v w) e. x))))
11	10	imp41 286	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ w e. B) -> (y -v w) e. x)
12	11	adantlr 310	. . . . . . . . . . . . . . . . . . . . 21 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> (y -v w) e. x)
13	12	adantr 306	. . . . . . . . . . . . . . . . . . . 20 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +v w)) -> (y -v w) e. x)
14		hvsubaddt 5042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((y -v w) = z <-> (w +v z) = y))
15		ax-hvcom 4985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((w e. H~ /\ z e. H~) -> (w +v z) = (z +v w))
16	15	cleq1d 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. H~ /\ z e. H~) -> ((w +v z) = y <-> (z +v w) = y))
17		cleqcom 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((z +v w) = y <-> y = (z +v w))
18	16, 17	syl6bb 414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. H~ /\ z e. H~) -> ((w +v z) = y <-> y = (z +v w)))
19	18	3adant1 597	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((w +v z) = y <-> y = (z +v w)))
20	14, 19	bitrd 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((y -v w) = z <-> y = (z +v w)))
21	20	3com23 616	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -v w) = z <-> y = (z +v w)))
22		chelt 5135	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. CH /\ y e. x) -> y e. H~)
23	22	adantlr 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((x e. CH /\ B (_ x) /\ y e. x) -> y e. H~)
24		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- A e. CH
25	24	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. A -> z e. H~)
26		sumdmdi.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- B e. CH
27	26	chel 5137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w e. B -> w e. H~)
28	21, 23, 25, 27	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A /\ w e. B) -> ((y -v w) = z <-> y = (z +v w)))
29	28	3expa 612	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> ((y -v w) = z <-> y = (z +v w)))
30		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y -v w) = z -> ((y -v w) e. x <-> z e. x))
31	29, 30	syl6bir 188	. . . . . . . . . . . . . . . . . . . . 21 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> (y = (z +v w) -> ((y -v w) e. x <-> z e. x)))
32	31	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +v w)) -> ((y -v w) e. x <-> z e. x))
33	13, 32	mpbid 170	. . . . . . . . . . . . . . . . . . 19 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +v w)) -> z e. x)
34		pm3.27 260	. . . . . . . . . . . . . . . . . . 19 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +v w)) -> y = (z +v w))
35	33, 34	jca 236	. . . . . . . . . . . . . . . . . 18 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +v w)) -> (z e. x /\ y = (z +v w)))
36	35	exp31 293	. . . . . . . . . . . . . . . . 17 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (w e. B -> (y = (z +v w) -> (z e. x /\ y = (z +v w)))))
37	36	r19.22dv 1278	. . . . . . . . . . . . . . . 16 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (E.w e. B y = (z +v w) -> E.w e. B (z e. x /\ y = (z +v w))))
38		r19.42v 1303	. . . . . . . . . . . . . . . 16 |- (E.w e. B (z e. x /\ y = (z +v w)) <-> (z e. x /\ E.w e. B y = (z +v w)))
39	37, 38	syl6ib 185	. . . . . . . . . . . . . . 15 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (E.w e. B y = (z +v w) -> (z e. x /\ E.w e. B y = (z +v w))))
40	39	r19.22dva 1280	. . . . . . . . . . . . . 14 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +v w) -> E.z e. A (z e. x /\ E.w e. B y = (z +v w))))
41		elin 1635	. . . . . . . . . . . . . . . . . 18 |- (z e. (x i^i A) <-> (z e. x /\ z e. A))
42		ancom 333	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ z e. A) <-> (z e. A /\ z e. x))
43	41, 42	bitr 151	. . . . . . . . . . . . . . . . 17 |- (z e. (x i^i A) <-> (z e. A /\ z e. x))
44	43	anbi1i 368	. . . . . . . . . . . . . . . 16 |- ((z e. (x i^i A) /\ E.w e. B y = (z +v w)) <-> ((z e. A /\ z e. x) /\ E.w e. B y = (z +v w)))
45		anass 336	. . . . . . . . . . . . . . . 16 |- (((z e. A /\ z e. x) /\ E.w e. B y = (z +v w)) <-> (z e. A /\ (z e. x /\ E.w e. B y = (z +v w))))
46	44, 45	bitr 151	. . . . . . . . . . . . . . 15 |- ((z e. (x i^i A) /\ E.w e. B y = (z +v w)) <-> (z e. A /\ (z e. x /\ E.w e. B y = (z +v w))))
47	46	birex2 1227	. . . . . . . . . . . . . 14 |- (E.z e. (x i^i A)E.w e. B y = (z +v w) <-> E.z e. A (z e. x /\ E.w e. B y = (z +v w)))
48	40, 47	syl6ibr 186	. . . . . . . . . . . . 13 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +v w) -> E.z e. (x i^i A)E.w e. B y = (z +v w)))
49	24	chshi 5132	. . . . . . . . . . . . . . . . 17 |- A e. SH
50		shinclt 5352	. . . . . . . . . . . . . . . . 17 |- ((x e. SH /\ A e. SH) -> (x i^i A) e. SH)
51	49, 50	mpan2 519	. . . . . . . . . . . . . . . 16 |- (x e. SH -> (x i^i A) e. SH)
52	3, 51	syl 12	. . . . . . . . . . . . . . 15 |- (x e. CH -> (x i^i A) e. SH)
53	52	ad2antll 320	. . . . . . . . . . . . . 14 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (x i^i A) e. SH)
54	26	chshi 5132	. . . . . . . . . . . . . . 15 |- B e. SH
55		shselt 5280	. . . . . . . . . . . . . . 15 |- (((x i^i A) e. SH /\ B e. SH) -> (y e. ((x i^i A) +H B) <-> E.z e. (x i^i A)E.w e. B y = (z +v w)))
56	54, 55	mpan2 519	. . . . . . . . . . . . . 14 |- ((x i^i A) e. SH -> (y e. ((x i^i A) +H B) <-> E.z e. (x i^i A)E.w e. B y = (z +v w)))
57	53, 56	syl 12	. . . . . . . . . . . . 13 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (y e. ((x i^i A) +H B) <-> E.z e. (x i^i A)E.w e. B y = (z +v w)))
58	48, 57	sylibrd 179	. . . . . . . . . . . 12 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +v w) -> y e. ((x i^i A) +H B)))
59	24, 26	chsel 5381	. . . . . . . . . . . 12 |- (y e. (A +H B) <-> E.z e. A E.w e. B y = (z +v w))
60	58, 59	syl5ib 181	. . . . . . . . . . 11 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (y e. (A +H B) -> y e. ((x i^i A) +H B)))
61	60	exp 291	. . . . . . . . . 10 |- ((x e. CH /\ B (_ x) -> (y e. x -> (y e. (A +H B)