Metamath Proof Explorer

Theorem dmdbr

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( y = A -> ( y e. CH <-> A e. CH ) )
2 1 anbi1d 
 |-  ( y = A -> ( ( y e. CH /\ z e. CH ) <-> ( A e. CH /\ z e. CH ) ) )
3 ineq2 
 |-  ( y = A -> ( x i^i y ) = ( x i^i A ) )
4 3 oveq1d 
 |-  ( y = A -> ( ( x i^i y ) vH z ) = ( ( x i^i A ) vH z ) )
5 oveq1 
 |-  ( y = A -> ( y vH z ) = ( A vH z ) )
6 5 ineq2d 
 |-  ( y = A -> ( x i^i ( y vH z ) ) = ( x i^i ( A vH z ) ) )
7 4 6 eqeq12d 
 |-  ( y = A -> ( ( ( x i^i y ) vH z ) = ( x i^i ( y vH z ) ) <-> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) )
8 7 imbi2d 
 |-  ( y = A -> ( ( z C_ x -> ( ( x i^i y ) vH z ) = ( x i^i ( y vH z ) ) ) <-> ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) ) )
9 8 ralbidv 
 |-  ( y = A -> ( A. x e. CH ( z C_ x -> ( ( x i^i y ) vH z ) = ( x i^i ( y vH z ) ) ) <-> A. x e. CH ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) ) )
10 2 9 anbi12d 
 |-  ( y = A -> ( ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( z C_ x -> ( ( x i^i y ) vH z ) = ( x i^i ( y vH z ) ) ) ) <-> ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) ) ) )
11 eleq1 
 |-  ( z = B -> ( z e. CH <-> B e. CH ) )
12 11 anbi2d 
 |-  ( z = B -> ( ( A e. CH /\ z e. CH ) <-> ( A e. CH /\ B e. CH ) ) )
13 sseq1 
 |-  ( z = B -> ( z C_ x <-> B C_ x ) )
14 oveq2 
 |-  ( z = B -> ( ( x i^i A ) vH z ) = ( ( x i^i A ) vH B ) )
15 oveq2 
 |-  ( z = B -> ( A vH z ) = ( A vH B ) )
16 15 ineq2d 
 |-  ( z = B -> ( x i^i ( A vH z ) ) = ( x i^i ( A vH B ) ) )
17 14 16 eqeq12d 
 |-  ( z = B -> ( ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) <-> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) )
18 13 17 imbi12d 
 |-  ( z = B -> ( ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) <-> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )
19 18 ralbidv 
 |-  ( z = B -> ( A. x e. CH ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) <-> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )
20 12 19 anbi12d 
 |-  ( z = B -> ( ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( z C_ x -> ( ( x i^i A ) vH z ) = ( x i^i ( A vH z ) ) ) ) <-> ( ( A e. CH /\ B e. CH ) /\ A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) ) )
21 df-dmd 
 |-  MH* = { <. y , z >. | ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( z C_ x -> ( ( x i^i y ) vH z ) = ( x i^i ( y vH z ) ) ) ) }
22 10 20 21 brabg 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> ( ( A e. CH /\ B e. CH ) /\ A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) ) )
23 22 bianabs 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )