Theorem sumdmdi 10342

Description: If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [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 2211	. . . . . . 7 |- ((A +H B) = (A vH B) -> (x i^i (A +H B)) = (x i^i (A vH B)))
2	1	adantr 389	. . . . . 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 9096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. CH -> x e. SH)
4		shsubcltOLD 9090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. SH -> ((y e. x /\ w e. x) -> (y -h w) e. x))
5	4	exp3a 375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. SH -> (y e. x -> (w e. x -> (y -h w) e. x)))
6	3, 5	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. CH -> (y e. x -> (w e. x -> (y -h w) e. x)))
7		ssel2 2064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((B (_ x /\ w e. B) -> w e. x)
8	6, 7	syl7 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. CH -> (y e. x -> ((B (_ x /\ w e. B) -> (y -h w) e. x)))
9	8	exp4a 378	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. CH -> (y e. x -> (B (_ x -> (w e. B -> (y -h w) e. x))))
10	9	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. CH -> (B (_ x -> (y e. x -> (w e. B -> (y -h w) e. x))))
11	10	imp41 368	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ w e. B) -> (y -h w) e. x)
12	11	adantlr 393	. . . . . . . . . . . . . . . . . . . . 21 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> (y -h w) e. x)
13	12	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +h w)) -> (y -h w) e. x)
14		hvsubaddt 8944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((y -h w) = z <-> (w +h z) = y))
15		ax-hvcom 8871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((w e. H~ /\ z e. H~) -> (w +h z) = (z +h w))
16	15	eqeq1d 1483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. H~ /\ z e. H~) -> ((w +h z) = y <-> (z +h w) = y))
17		eqcom 1477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((z +h w) = y <-> y = (z +h w))
18	16, 17	syl6bb 536	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. H~ /\ z e. H~) -> ((w +h z) = y <-> y = (z +h w)))
19	18	3adant1 797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((w +h z) = y <-> y = (z +h w)))
20	14, 19	bitrd 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. H~ /\ w e. H~ /\ z e. H~) -> ((y -h w) = z <-> y = (z +h w)))
21	20	3com23 839	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. H~ /\ z e. H~ /\ w e. H~) -> ((y -h w) = z <-> y = (z +h w)))
22		chelt 9100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. CH /\ y e. x) -> y e. H~)
23	22	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((x e. CH /\ B (_ x) /\ y e. x) -> y e. H~)
24		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- A e. CH
25	24	chel 9102	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. A -> z e. H~)
26		sumdmdi.2	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- B e. CH
27	26	chel 9102	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w e. B -> w e. H~)
28	21, 23, 25, 27	syl3an 868	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A /\ w e. B) -> ((y -h w) = z <-> y = (z +h w)))
29	28	3expa 833	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> ((y -h w) = z <-> y = (z +h w)))
30		eleq1 1534	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y -h w) = z -> ((y -h w) e. x <-> z e. x))
31	29, 30	syl6bir 215	. . . . . . . . . . . . . . . . . . . . 21 |- (((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) -> (y = (z +h w) -> ((y -h w) e. x <-> z e. x)))
32	31	imp 350	. . . . . . . . . . . . . . . . . . . 20 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +h w)) -> ((y -h w) e. x <-> z e. x))
33	13, 32	mpbid 195	. . . . . . . . . . . . . . . . . . 19 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +h w)) -> z e. x)
34		pm3.27 323	. . . . . . . . . . . . . . . . . . 19 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +h w)) -> y = (z +h w))
35	33, 34	jca 288	. . . . . . . . . . . . . . . . . 18 |- ((((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) /\ w e. B) /\ y = (z +h w)) -> (z e. x /\ y = (z +h w)))
36	35	exp31 376	. . . . . . . . . . . . . . . . 17 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (w e. B -> (y = (z +h w) -> (z e. x /\ y = (z +h w)))))
37	36	r19.22dv 1737	. . . . . . . . . . . . . . . 16 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (E.w e. B y = (z +h w) -> E.w e. B (z e. x /\ y = (z +h w))))
38		r19.42v 1764	. . . . . . . . . . . . . . . 16 |- (E.w e. B (z e. x /\ y = (z +h w)) <-> (z e. x /\ E.w e. B y = (z +h w)))
39	37, 38	syl6ib 212	. . . . . . . . . . . . . . 15 |- ((((x e. CH /\ B (_ x) /\ y e. x) /\ z e. A) -> (E.w e. B y = (z +h w) -> (z e. x /\ E.w e. B y = (z +h w))))
40	39	r19.22dva 1739	. . . . . . . . . . . . . 14 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +h w) -> E.z e. A (z e. x /\ E.w e. B y = (z +h w))))
41		elin 2207	. . . . . . . . . . . . . . . . . 18 |- (z e. (x i^i A) <-> (z e. x /\ z e. A))
42		ancom 435	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ z e. A) <-> (z e. A /\ z e. x))
43	41, 42	bitr 173	. . . . . . . . . . . . . . . . 17 |- (z e. (x i^i A) <-> (z e. A /\ z e. x))
44	43	anbi1i 481	. . . . . . . . . . . . . . . 16 |- ((z e. (x i^i A) /\ E.w e. B y = (z +h w)) <-> ((z e. A /\ z e. x) /\ E.w e. B y = (z +h w)))
45		anass 439	. . . . . . . . . . . . . . . 16 |- (((z e. A /\ z e. x) /\ E.w e. B y = (z +h w)) <-> (z e. A /\ (z e. x /\ E.w e. B y = (z +h w))))
46	44, 45	bitr 173	. . . . . . . . . . . . . . 15 |- ((z e. (x i^i A) /\ E.w e. B y = (z +h w)) <-> (z e. A /\ (z e. x /\ E.w e. B y = (z +h w))))
47	46	rexbii2 1672	. . . . . . . . . . . . . 14 |- (E.z e. (x i^i A)E.w e. B y = (z +h w) <-> E.z e. A (z e. x /\ E.w e. B y = (z +h w)))
48	40, 47	syl6ibr 213	. . . . . . . . . . . . 13 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +h w) -> E.z e. (x i^i A)E.w e. B y = (z +h w)))
49	24	chshi 9097	. . . . . . . . . . . . . . . . 17 |- A e. SH
50		shinclt 9351	. . . . . . . . . . . . . . . . 17 |- ((x e. SH /\ A e. SH) -> (x i^i A) e. SH)
51	49, 50	mpan2 696	. . . . . . . . . . . . . . . 16 |- (x e. SH -> (x i^i A) e. SH)
52	3, 51	syl 10	. . . . . . . . . . . . . . 15 |- (x e. CH -> (x i^i A) e. SH)
53	52	ad2antrr 404	. . . . . . . . . . . . . 14 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (x i^i A) e. SH)
54	26	chshi 9097	. . . . . . . . . . . . . . 15 |- B e. SH
55		shselt 9278	. . . . . . . . . . . . . . 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 +h w)))
56	54, 55	mpan2 696	. . . . . . . . . . . . . 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 +h w)))
57	53, 56	syl 10	. . . . . . . . . . . . 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 +h w)))
58	48, 57	sylibrd 204	. . . . . . . . . . . 12 |- (((x e. CH /\ B (_ x) /\ y e. x) -> (E.z e. A E.w e. B y = (z +h w) -> y e. ((x i^i A) +H B)))
59	24, 26	chsel 9382	. . . . . . . . . . . 12 |- (y e. (A +H B) <-> E.z e. A E.w e. B y = (z +h w))
60	58, 59	syl5ib 206	. . . . . . . . . . 11 |- (((x e. CH /\ B (_