HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem dmdbr5 10226
Description: Binary relation expressing the dual modular pair property.
Assertion
Ref Expression
dmdbr5 |- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
Distinct variable groups:   x,A   x,B
Proof of Theorem dmdbr5
StepHypRef Expression
1 dmdbr4 10224 . . 3 |- ((A e. CH /\ B e. CH) -> (A MH* B <-> A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
2 ssin 2230 . . . . . . . . 9 |- ((x (_ (x vH B) /\ x (_ (A vH B)) <-> x (_ ((x vH B) i^i (A vH B)))
3 sstr2 2069 . . . . . . . . 9 |- (x (_ ((x vH B) i^i (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
42, 3sylbi 199 . . . . . . . 8 |- ((x (_ (x vH B) /\ x (_ (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
5 chub1t 9418 . . . . . . . . 9 |- ((x e. CH /\ B e. CH) -> x (_ (x vH B))
65ancoms 436 . . . . . . . 8 |- ((B e. CH /\ x e. CH) -> x (_ (x vH B))
74, 6sylan 448 . . . . . . 7 |- (((B e. CH /\ x e. CH) /\ x (_ (A vH B)) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B)))
87ex 373 . . . . . 6 |- ((B e. CH /\ x e. CH) -> (x (_ (A vH B) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> x (_ (((x vH B) i^i A) vH B))))
98com23 32 . . . . 5 |- ((B e. CH /\ x e. CH) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
109r19.20dva 1708 . . . 4 |- (B e. CH -> (A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
1110adantl 388 . . 3 |- ((A e. CH /\ B e. CH) -> (A.x e. CH ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
121, 11sylbid 203 . 2 |- ((A e. CH /\ B e. CH) -> (A MH* B -> A.x e. CH (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B))))
13 chjclt 9317 . . . . . . . . . . . 12 |- ((y e. CH /\ B e. CH) -> (y vH B) e. CH)
1413ancoms 436 . . . . . . . . . . 11 |- ((B e. CH /\ y e. CH) -> (y vH B) e. CH)
1514adantll 392 . . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (y vH B) e. CH)
16 chjclt 9317 . . . . . . . . . . 11 |- ((A e. CH /\ B e. CH) -> (A vH B) e. CH)
1716adantr 389 . . . . . . . . . 10 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (A vH B) e. CH)
1815, 17jca 288 . . . . . . . . 9 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((y vH B) e. CH /\ (A vH B) e. CH))
19 chinclt 9410 . . . . . . . . 9 |- (((y vH B) e. CH /\ (A vH B) e. CH) -> ((y vH B) i^i (A vH B)) e. CH)
20 inss2 2229 . . . . . . . . . 10 |- ((y vH B) i^i (A vH B)) (_ (A vH B)
21 pm2.27 62 . . . . . . . . . 10 |- (((y vH B) i^i (A vH B)) e. CH -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))))
2220, 21mpii 45 . . . . . . . . 9 |- (((y vH B) i^i (A vH B)) e. CH -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B)))
2318, 19, 223syl 20 . . . . . . . 8 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((((y vH B) i^i (A vH B)) e. CH -> (((y vH B) i^i (A vH B)) (_ (A vH B) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B))) -> ((y vH B) i^i (A vH B)) (_ (((((y vH B) i^i (A vH B)) vH B) i^i A) vH B)))
24 chub2t 9419 . . . . . . . . . . . . . . . 16 |- ((B e. CH /\ y e. CH) -> B (_ (y vH B))
2524adantll 392 . . . . . . . . . . . . . . 15 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ (y vH B))
26 chub2t 9419 . . . . . . . . . . . . . . . . 17 |- ((B e. CH /\ A e. CH) -> B (_ (A vH B))
2726ancoms 436 . . . . . . . . . . . . . . . 16 |- ((A e. CH /\ B e. CH) -> B (_ (A vH B))
2827adantr 389 . . . . . . . . . . . . . . 15 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ (A vH B))
2925, 28jca 288 . . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (B (_ (y vH B) /\ B (_ (A vH B)))
30 ssin 2230 . . . . . . . . . . . . . 14 |- ((B (_ (y vH B) /\ B (_ (A vH B)) <-> B (_ ((y vH B) i^i (A vH B)))
3129, 30sylib 198 . . . . . . . . . . . . 13 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B (_ ((y vH B) i^i (A vH B)))
32 chlejb2t 9424 . . . . . . . . . . . . . 14 |- ((B e. CH /\ ((y vH B) i^i (A vH B)) e. CH) -> (B (_ ((y vH B) i^i (A vH B)) <-> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B))))
33 simplr 413 . . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> B e. CH)
3419, 15, 17sylanc 471 . . . . . . . . . . . . . 14 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((y vH B) i^i (A vH B)) e. CH)
3532, 33, 34sylanc 471 . . . . . . . . . . . . 13 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (B (_ ((y vH B) i^i (A vH B)) <-> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B))))
3631, 35mpbid 195 . . . . . . . . . . . 12 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> (((y vH B) i^i (A vH B)) vH B) = ((y vH B) i^i (A vH B)))
3736ineq1d 2214 . . . . . . . . . . 11 |- (((A e. CH /\ B e. CH) /\ y e. CH) -> ((((y vH B) i^i (A vH B)) vH B) i^i A) = (((y vH B) i^i (A vH B)) i^i A))
38 chabs2t 9428 . . . . . . . . . . . . . . 15 |- ((A e. CH /\ B e. CH) -> (A i^i (A vH B)) = A)
39 incom 2206 . . . . . . . . . . . . . . 15 |- ((A vH B) i^i A) = (A i^i (A vH B))
4038, 39syl5eq 1518 . . . . . . . . . . . . . 14 |- ((A e. CH /\ B e. CH) -> ((A vH B) i^i A) = A)
4140ineq2d 2215 . . . . . . . . . . . . 13 |- ((A e. CH /\ B e. CH) -> ((y vH B) i^i ((A vH B) i^i A)) = ((y vH B) i^i A))
42 inass 2221 . . . . . . . . . . . . 13 |- (((y vH B) i^i (A vH B)) i^i A) = ((y vH B) i^i ((A vH B) i^i A))
4341, 42syl5eq 1518 . . . . . . . . . . . 12 |- ((A e. CH /\ B e. CH) -> (((y vH B) i^i (A vH B)) i^i A) = ((y vH B) i^i A))
4443adantr 389 . . . . . . . . . . 11 |- (((