Theorem sumdmd 5787

Description: The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519.

Hypotheses

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

Assertion

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

Proof of Theorem sumdmd

Step	Hyp	Ref	Expression
1		sumdmdi.1	. . 3 |- A e. CH
2		sumdmdi.2	. . 3 |- B e. CH
3	1, 2	sumdmdi 5785	. 2 |- ((A +H B) = (A vH B) -> (_|_` A) MH (_|_` B))
4		spansnsht 5466	. . . . . . . . . . . . . 14 |- (x e. H~ -> (span` {x}) e. SH)
5	2	chshi 5132	. . . . . . . . . . . . . . 15 |- B e. SH
6		shsub2t 5290	. . . . . . . . . . . . . . 15 |- (((span` {x}) e. SH /\ B e. SH) -> (span` {x}) (_ (B +H (span` {x})))
7	5, 6	mpan2 519	. . . . . . . . . . . . . 14 |- ((span` {x}) e. SH -> (span` {x}) (_ (B +H (span` {x})))
8	4, 7	syl 12	. . . . . . . . . . . . 13 |- (x e. H~ -> (span` {x}) (_ (B +H (span` {x})))
9		spansnid 5468	. . . . . . . . . . . . 13 |- (x e. H~ -> x e. (span` {x}))
10	8, 9	sseldd 1507	. . . . . . . . . . . 12 |- (x e. H~ -> x e. (B +H (span` {x})))
11	10	ad2antrl 322	. . . . . . . . . . 11 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> x e. (B +H (span` {x})))
12		shsub1t 5289	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. SH /\ (span` {x}) e. SH) -> B (_ (B +H (span` {x})))
13	5, 12	mpan 518	. . . . . . . . . . . . . . . . . . 19 |- ((span` {x}) e. SH -> B (_ (B +H (span` {x})))
14	4, 13	syl 12	. . . . . . . . . . . . . . . . . 18 |- (x e. H~ -> B (_ (B +H (span` {x})))
15		spansnsclt 5541	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. CH /\ x e. H~) -> (B +H (span` {x})) e. CH)
16	2, 15	mpan 518	. . . . . . . . . . . . . . . . . . 19 |- (x e. H~ -> (B +H (span` {x})) e. CH)
17		dmdi 5732	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CH /\ B e. CH /\ (B +H (span` {x})) e. CH) -> ((_|_` A) MH (_|_` B) -> (B (_ (B +H (span` {x})) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))))
18	1, 17	mp3an1 639	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. CH /\ (B +H (span` {x})) e. CH) -> ((_|_` A) MH (_|_` B) -> (B (_ (B +H (span` {x})) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))))
19	2, 18	mpan 518	. . . . . . . . . . . . . . . . . . 19 |- ((B +H (span` {x})) e. CH -> ((_|_` A) MH (_|_` B) -> (B (_ (B +H (span` {x})) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))))
20	16, 19	syl 12	. . . . . . . . . . . . . . . . . 18 |- (x e. H~ -> ((_|_` A) MH (_|_` B) -> (B (_ (B +H (span` {x})) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))))
21	14, 20	mpid 48	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((_|_` A) MH (_|_` B) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B))))
22	21	com12 13	. . . . . . . . . . . . . . . 16 |- ((_|_` A) MH (_|_` B) -> (x e. H~ -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B))))
23	22	imp 277	. . . . . . . . . . . . . . 15 |- (((_|_` A) MH (_|_` B) /\ x e. H~) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))
24	23	adantrr 312	. . . . . . . . . . . . . 14 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> (((B +H (span` {x})) i^i A) vH B) = ((B +H (span` {x})) i^i (A vH B)))
25	1	chshi 5132	. . . . . . . . . . . . . . . . 17 |- A e. SH
26	5, 25	shsub2 5343	. . . . . . . . . . . . . . . 16 |- B (_ (A +H B)
27	1, 2	sumdmdlem 5786	. . . . . . . . . . . . . . . . . . 19 |- ((x e. H~ /\ -. x e. (A +H B)) -> ((B +H (span` {x})) i^i A) = (B i^i A))
28	27	opreq1d 3012	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ -. x e. (A +H B)) -> (((B +H (span` {x})) i^i A) vH B) = ((B i^i A) vH B))
29	2, 1	chincl 5382	. . . . . . . . . . . . . . . . . . . 20 |- (B i^i A) e. CH
30	29, 2	chjcom 5389	. . . . . . . . . . . . . . . . . . 19 |- ((B i^i A) vH B) = (B vH (B i^i A))
31	2, 1	chabs1 5434	. . . . . . . . . . . . . . . . . . 19 |- (B vH (B i^i A)) = B
32	30, 31	eqtr 1119	. . . . . . . . . . . . . . . . . 18 |- ((B i^i A) vH B) = B
33	28, 32	syl6eq 1140	. . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ -. x e. (A +H B)) -> (((B +H (span` {x})) i^i A) vH B) = B)
34	33	sseq1d 1527	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ -. x e. (A +H B)) -> ((((B +H (span` {x})) i^i A) vH B) (_ (A +H B) <-> B (_ (A +H B)))
35	26, 34	mpbiri 169	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ -. x e. (A +H B)) -> (((B +H (span` {x})) i^i A) vH B) (_ (A +H B))
36	35	adantl 305	. . . . . . . . . . . . . 14 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> (((B +H (span` {x})) i^i A) vH B) (_ (A +H B))
37	24, 36	eqsstr3d 1535	. . . . . . . . . . . . 13 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> ((B +H (span` {x})) i^i (A vH B)) (_ (A +H B))
38	37	sseld 1506	. . . . . . . . . . . 12 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> (x e. ((B +H (span` {x})) i^i (A vH B)) -> x e. (A +H B)))
39		elin 1635	. . . . . . . . . . . 12 |- (x e. ((B +H (span` {x})) i^i (A vH B)) <-> (x e. (B +H (span` {x})) /\ x e. (A vH B)))
40	38, 39	syl5ibr 182	. . . . . . . . . . 11 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> ((x e. (B +H (span` {x})) /\ x e. (A vH B)) -> x e. (A +H B)))
41	11, 40	mpand 524	. . . . . . . . . 10 |- (((_|_` A) MH (_|_` B) /\ (x e. H~ /\ -. x e. (A +H B))) -> (x e. (A vH B) -> x e. (A +H B)))
42	41	exp32 294	. . . . . . . . 9 |- ((_|_` A) MH (_|_` B) -> (x e. H~ -> (-. x e. (A +H B) -> (x e. (A vH B) -> x e. (A +H B)))))
43	42	com34 36	. . . . . . . 8 |- ((_|_` A) MH (_|_` B) -> (x e. H~ -> (x e. (A vH B) -> (-. x e. (A +H B) -> x e. (A +H B)))))
44		pm2.18 75	. . . . . . . 8 |- ((-. x e. (A +H B) -> x e. (A +H B)) -> x e. (A +H B))
45	43, 44	syl8 25	. . . . . . 7 |- ((_|_` A) MH (_|_` B) -> (x e. H~ -> (x e. (A vH B) -> x e. (A +H B))))
46	1, 2	chjcl 5379	. . . . . . . 8 |- (A vH B) e. CH
47	46	chel 5137	. . . . . . 7 |- (x e. (A vH B) -> x e. H~)
48	45, 47	syl5 22	. . . . . 6 |- ((_|_` A) MH (_|_` B) -> (x e. (A vH B) -> (x e. (A vH B) -> x e. (A +H B))))
49	48	pm2.43d 59	. . . . 5 |- ((_|_` A) MH (_|_` B) -> (x e. (A vH B) -> x e. (A +H B)))
50	49	ssrdv 1509	. . . 4 |- ((_|_` A) MH (_|_` B) -> (A vH B) (_ (A +H B))
51	1, 2	chslej 5380	. . . 4 |- (A +H B) (_ (A vH B)
52	50, 51	jctil 240	. . 3 |- ((_|_` A) MH (_|_` B) -> ((A +H B) (_ (A vH B) /\ (A vH B) (_ (A +H B)))
53		eqss 1516	. . 3 |- ((A +H B) = (A vH B) <-> ((A +H B) (_ (A vH B) /\ (A vH B) (_ (A +H B)))
54	52, 53	sylibr 175	. 2 |- ((_|_` A) MH (_|_` B) -> (A +H B) = (A vH B))
55	3, 54	impbi 139	1 |- ((A +H B) = (A vH B) <-> (_|_` A) MH (_|_` B))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196   = wceq 1091   e. wcel 1092   i^i cin 1486   (_ wss 1487  {