This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdbr

Description: Binary relation expressing <. A , B >. is a modular pair. Definition 1.1 of MaedaMaeda p. 1. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdbr 
|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i 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 oveq2 
 |-  ( y = A -> ( x vH y ) = ( x vH A ) )
4 3 ineq1d 
 |-  ( y = A -> ( ( x vH y ) i^i z ) = ( ( x vH A ) i^i z ) )
5 ineq1 
 |-  ( y = A -> ( y i^i z ) = ( A i^i z ) )
6 5 oveq2d 
 |-  ( y = A -> ( x vH ( y i^i z ) ) = ( x vH ( A i^i z ) ) )
7 4 6 eqeq12d 
 |-  ( y = A -> ( ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) <-> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) )
8 7 imbi2d 
 |-  ( y = A -> ( ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) <-> ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) )
9 8 ralbidv 
 |-  ( y = A -> ( A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) <-> A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) )
10 2 9 anbi12d 
 |-  ( y = A -> ( ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) ) <-> ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i 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 sseq2 
 |-  ( z = B -> ( x C_ z <-> x C_ B ) )
14 ineq2 
 |-  ( z = B -> ( ( x vH A ) i^i z ) = ( ( x vH A ) i^i B ) )
15 ineq2 
 |-  ( z = B -> ( A i^i z ) = ( A i^i B ) )
16 15 oveq2d 
 |-  ( z = B -> ( x vH ( A i^i z ) ) = ( x vH ( A i^i B ) ) )
17 14 16 eqeq12d 
 |-  ( z = B -> ( ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) <-> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
18 13 17 imbi12d 
 |-  ( z = B -> ( ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) <-> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
19 18 ralbidv 
 |-  ( z = B -> ( A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
20 12 19 anbi12d 
 |-  ( z = B -> ( ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) <-> ( ( A e. CH /\ B e. CH ) /\ A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
21 df-md 
 |-  MH = { <. y , z >. | ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i 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 ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
23 22 bianabs 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )