Metamath Proof Explorer

Theorem mddmd2

Description: Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mddmd2 
|- ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A MH* x ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = y -> ( A MH x <-> A MH y ) )
2 1 cbvralvw 
 |-  ( A. x e. CH A MH x <-> A. y e. CH A MH y )
3 mdbr 
 |-  ( ( A e. CH /\ y e. CH ) -> ( A MH y <-> A. x e. CH ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) ) )
4 chjcom 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A vH x ) = ( x vH A ) )
5 4 ineq1d 
 |-  ( ( A e. CH /\ x e. CH ) -> ( ( A vH x ) i^i y ) = ( ( x vH A ) i^i y ) )
6 incom 
 |-  ( ( A vH x ) i^i y ) = ( y i^i ( A vH x ) )
7 5 6 eqtr3di 
 |-  ( ( A e. CH /\ x e. CH ) -> ( ( x vH A ) i^i y ) = ( y i^i ( A vH x ) ) )
8 7 adantlr 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( x vH A ) i^i y ) = ( y i^i ( A vH x ) ) )
9 chincl 
 |-  ( ( A e. CH /\ y e. CH ) -> ( A i^i y ) e. CH )
10 chjcom 
 |-  ( ( ( A i^i y ) e. CH /\ x e. CH ) -> ( ( A i^i y ) vH x ) = ( x vH ( A i^i y ) ) )
11 9 10 sylan 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( A i^i y ) vH x ) = ( x vH ( A i^i y ) ) )
12 incom 
 |-  ( A i^i y ) = ( y i^i A )
13 12 oveq1i 
 |-  ( ( A i^i y ) vH x ) = ( ( y i^i A ) vH x )
14 11 13 eqtr3di 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( x vH ( A i^i y ) ) = ( ( y i^i A ) vH x ) )
15 8 14 eqeq12d 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) <-> ( y i^i ( A vH x ) ) = ( ( y i^i A ) vH x ) ) )
16 eqcom 
 |-  ( ( y i^i ( A vH x ) ) = ( ( y i^i A ) vH x ) <-> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) )
17 15 16 bitrdi 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) <-> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) )
18 17 imbi2d 
 |-  ( ( ( A e. CH /\ y e. CH ) /\ x e. CH ) -> ( ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) <-> ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
19 18 ralbidva 
 |-  ( ( A e. CH /\ y e. CH ) -> ( A. x e. CH ( x C_ y -> ( ( x vH A ) i^i y ) = ( x vH ( A i^i y ) ) ) <-> A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
20 3 19 bitrd 
 |-  ( ( A e. CH /\ y e. CH ) -> ( A MH y <-> A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
21 20 ralbidva 
 |-  ( A e. CH -> ( A. y e. CH A MH y <-> A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
22 2 21 syl5bb 
 |-  ( A e. CH -> ( A. x e. CH A MH x <-> A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
23 ralcom 
 |-  ( A. y e. CH A. x e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) )
24 22 23 bitrdi 
 |-  ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
25 dmdbr 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A MH* x <-> A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
26 25 ralbidva 
 |-  ( A e. CH -> ( A. x e. CH A MH* x <-> A. x e. CH A. y e. CH ( x C_ y -> ( ( y i^i A ) vH x ) = ( y i^i ( A vH x ) ) ) ) )
27 24 26 bitr4d 
 |-  ( A e. CH -> ( A. x e. CH A MH x <-> A. x e. CH A MH* x ) )