Theorem dmdbr 5731

Description: Binary relation expressing the dual modular pair property. Remark 29.6 of [MaedaMaeda] p. 130. We will use the idiom (_|_` A) MH (_|_` B) to mean A and B are a dual modular pair, since the equivalence happens to hold in Hilbert lattices, as this theorem shows.

Assertion

Ref	Expression
dmdbr	|- ((A e. CH /\ B e. CH) -> ((_|_` A) MH (_|_` B) <-> A.x e. CH (B (_ x -> ((x i^i A) vH B) = (x i^i (A vH B)))))

Distinct variable group(s):   x,A   x,B

Proof of Theorem dmdbr

Step	Hyp	Ref	Expression
1		mdbr 5726	. . 3 |- (((_|_` A) e. CH /\ (_|_` B) e. CH) -> ((_|_` A) MH (_|_` B) <-> A.y e. CH (y (_ (_|_` B) -> ((y vH (_|_` A)) i^i (_|_` B)) = (y vH ((_|_` A) i^i (_|_` B))))))
2		choclt 5191	. . 3 |- (A e. CH -> (_|_` A) e. CH)
3		choclt 5191	. . 3 |- (B e. CH -> (_|_` B) e. CH)
4	1, 2, 3	syl2an 349	. 2 |- ((A e. CH /\ B e. CH) -> ((_|_` A) MH (_|_` B) <-> A.y e. CH (y (_ (_|_` B) -> ((y vH (_|_` A)) i^i (_|_` B)) = (y vH ((_|_` A) i^i (_|_` B))))))
5		choclt 5191	. . . . . . . . . . 11 |- (x e. CH -> (_|_` x) e. CH)
6	5	syl4 19	. . . . . . . . . 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))))))
7	6	com12 13	. . . . . . . . 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))))))
8	7	adantl 305	. . . . . . . 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))))))
9		chsscon3t 5417	. . . . . . . . . . 11 |- ((B e. CH /\ x e. CH) -> (B (_ x <-> (_|_` x) (_ (_|_` B)))
10	9	biimpd 135	. . . . . . . . . 10 |- ((B e. CH /\ x e. CH) -> (B (_ x -> (_|_` x) (_ (_|_` B)))
11	10	adantll 309	. . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (B (_ x -> (_|_` x) (_ (_|_` B)))
12		chdmm3t 5440	. . . . . . . . . . . . . . 15 |- ((((_|_` x) vH (_|_` A)) e. CH /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((_|_` ((_|_` x) vH (_|_` A))) vH B))
13		chjclt 5330	. . . . . . . . . . . . . . . 16 |- (((_|_` x) e. CH /\ (_|_` A) e. CH) -> ((_|_` x) vH (_|_` A)) e. CH)
14	13, 5, 2	syl2an 349	. . . . . . . . . . . . . . 15 |- ((x e. CH /\ A e. CH) -> ((_|_` x) vH (_|_` A)) e. CH)
15	12, 14	sylan 343	. . . . . . . . . . . . . 14 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((_|_` ((_|_` x) vH (_|_` A))) vH B))
16		chdmj4t 5445	. . . . . . . . . . . . . . . 16 |- ((x e. CH /\ A e. CH) -> (_|_` ((_|_` x) vH (_|_` A))) = (x i^i A))
17	16	adantr 306	. . . . . . . . . . . . . . 15 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` ((_|_` x) vH (_|_` A))) = (x i^i A))
18	17	opreq1d 3012	. . . . . . . . . . . . . 14 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> ((_|_` ((_|_` x) vH (_|_` A))) vH B) = ((x i^i A) vH B))
19	15, 18	eqtrd 1128	. . . . . . . . . . . . 13 |- (((x e. CH /\ A e. CH) /\ B e. CH) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((x i^i A) vH B))
20	19	anasss 337	. . . . . . . . . . . 12 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` (((_|_` x) vH (_|_` A)) i^i (_|_` B))) = ((x i^i A) vH B))
21		chdmj2t 5443	. . . . . . . . . . . . . 14 |- ((x e. CH /\ ((_|_` A) i^i (_|_` B)) e. CH) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (_|_` ((_|_` A) i^i (_|_` B)))))
22		chinclt 5416	. . . . . . . . . . . . . . 15 |- (((_|_` A) e. CH /\ (_|_` B) e. CH) -> ((_|_` A) i^i (_|_` B)) e. CH)
23	22, 2, 3	syl2an 349	. . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> ((_|_` A) i^i (_|_` B)) e. CH)
24	21, 23	sylan2 346	. . . . . . . . . . . . 13 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (_|_` ((_|_` A) i^i (_|_` B)))))
25		chdmm4t 5441	. . . . . . . . . . . . . . 15 |- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) i^i (_|_` B))) = (A vH B))
26	25	adantl 305	. . . . . . . . . . . . . 14 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` A) i^i (_|_` B))) = (A vH B))
27	26	ineq2d 1645	. . . . . . . . . . . . 13 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (x i^i (_|_` ((_|_` A) i^i (_|_` B)))) = (x i^i (A vH B)))
28	24, 27	eqtrd 1128	. . . . . . . . . . . 12 |- ((x e. CH /\ (A e. CH /\ B e. CH)) -> (_|_` ((_|_` x) vH ((_|_` A) i^i (_|_` B)))) = (x i^i (A vH B)))
29	20, 28	cleq12d 1115	. . . . . . . . . . 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))))
30	29	ancoms 334	. . . . . . . . . 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))))
31		fveq2 2832	. . . . . . . . . 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)))))
32	30, 31	syl5bi 183	. . . . . . . . 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))))
33	11, 32	syl34d 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)))))
34	8, 33	syld 27	. . . . . . 7 |- (((A e. CH /\ B e. CH) /\ x e. CH) -> (((_|_` x) e. CH -> ((_|_` x) (_ (_|_` B) -> (((_|_` x) vH (_|_` A)) i^i (_|_` B)) = ((