HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem dmdmdt 10183
Description: The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of [MaedaMaeda] p. 130.
Assertion
Ref Expression
dmdmdt |- ((A e. CH /\ B e. CH) -> (A MH* B <-> (_|_` A) MH (_|_` B)))
Proof of Theorem dmdmdt
StepHypRef Expression
1 chocclt 9139 . . . . . . . . . . 11 |- (x e. CH -> (_|_` x) e. CH)
21imim1i 16 . . . . . . . . . 10 |- (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))) -> (x e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))))
32com12 11 . . . . . . . . 9 |- (x e. CH -> (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))) -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))))
43adantl 388 . . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))) -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))))
5 chsscon3t 9378 . . . . . . . . . . 11 |- ((B e. CH /\ x e. CH) -> (B (_ x <-> (_|_` x) (_ (_|_` B)))
65biimpd 153 . . . . . . . . . 10 |- ((B e. CH /\ x e. CH) -> (B (_ x -> (_|_` x) (_ (_|_` B)))
76adantll 392 . . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (B (_ x -> (_|_` x) (_ (_|_` B)))
8 chdmm3t 9405 . . . . . . . . . . . . . . 15 |- ((((_|_` x) vH (_|_` A)) e. CH /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((_|_` ((_|_` x) vH (_|_` A))) vH B))
9 chjclt 9284 . . . . . . . . . . . . . . . 16 |- (((_|_` x) e. CH /\ (_|_` A) e. CH) -> ((_|_` x) vH (_|_` A)) e. CH)
10 chocclt 9139 . . . . . . . . . . . . . . . 16 |- (A e. CH -> (_|_` A) e. CH)
119, 1, 10syl2an 454 . . . . . . . . . . . . . . 15 |- ((x e. CH /\ A e. CH) -> ((_|_` x) vH (_|_` A)) e. CH)
128, 11sylan 448 . . . . . . . . . . . . . 14 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((_|_` ((_|_` x) vH (_|_` A))) vH B))
13 chdmj4t 9410 . . . . . . . . . . . . . . . 16 |- ((x e. CH /\ A e. CH) -> (_|_` ((_|_` x) vH (_|_` A))) = (x i^i A))
1413adantr 389 . . . . . . . . . . . . . . 15 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` ((_|_` x) vH (_|_` A))) = (x i^i A))
1514opreq1d 3970 . . . . . . . . . . . . . 14 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> ((_|_` ((_|_` x) vH (_|_` A))) vH B) = ((x i^i A) vH B))
1612, 15eqtrd 1505 . . . . . . . . . . . . 13 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((x i^i A) vH B))
1716anasss 440 . . . . . . . . . . . 12 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((x i^i A) vH B))
18 chdmj2t 9408 . . . . . . . . . . . . . 14 |- ((x e. CH /\ ((_|_` A) i^i (_|_` B)) e. CH) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (_|_` ((_|_` A) i^i (_|_` B)))))
19 chinclt 9377 . . . . . . . . . . . . . . 15 |- (((_|_` A) e. CH /\ (_|_` B) e. CH) -> ((_|_` A) i^i (_|_` B)) e. CH)
20 chocclt 9139 . . . . . . . . . . . . . . 15 |- (B e. CH -> (_|_` B) e. CH)
2119, 10, 20syl2an 454 . . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> ((_|_` A) i^i (_|_` B)) e. CH)
2218, 21sylan2 451 . . . . . . . . . . . . 13 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (_|_` ((_|_` A) i^i (_|_` B)))))
23 chdmm4t 9406 . . . . . . . . . . . . . . 15 |- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) i^i (_|_` B))) = (A vH B))
2423adantl 388 . . . . . . . . . . . . . 14 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` A) i^i (_|_` B))) = (A vH B))
2524ineq2d 2214 . . . . . . . . . . . . 13 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (x i^i (_|_` ((_|_` A) i^i (_|_` B)))) = (x i^i (A vH B)))
2622, 25eqtrd 1505 . . . . . . . . . . . 12 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (A vH B)))
2717, 26eqeq12d 1487 . . . . . . . . . . 11 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> ((_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) <-> ((x i^i A) vH B) = (x i^i (A vH B))))
2827ancoms 436 . . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) <-> ((x i^i A) vH B) = (x i^i (A vH B))))
29 fveq2 3719 . . . . . . . . . 10 |- ((((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))))
3028, 29syl5bi 208 . . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> ((((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))) -> ((x i^i A) vH B) = (x i^i (A vH B))))
317, 30imim12d 29 . . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) -> (B (_ x -> ((x i^i A) vH B) = (x i^i (A vH B)))))
324, 31syld 27 . . . . . . 7 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))) -> (B (_ x -> ((x i^i A) vH B) = (x i^i (A vH B)))))
3332ex 373 . . . . . 6 |- ((A e. CH /\ B e. CH) -> (x e. CH -> (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((_|_` x) vH ((_|_` A) i^i (_|_` B))))) -> (B (_ x -> ((x i^i A) vH B) = (x i^i (A vH B))))))
3433com23 32 . . . . 5 |- ((A e. CH /\