Metamath Proof Explorer

Theorem dmdsl3

Description: Sublattice mapping for a dual-modular pair. Part of Theorem 1.3 of MaedaMaeda p. 2. (Contributed by NM, 26-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dmdi 
 |-  ( ( ( B e. CH /\ A e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
2 1 exp32 
 |-  ( ( B e. CH /\ A e. CH /\ C e. CH ) -> ( B MH* A -> ( A C_ C -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) ) ) )
3 2 3com12 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B MH* A -> ( A C_ C -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) ) ) )
4 3 imp32 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
5 4 3adantr3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
6 chjcom 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) = ( B vH A ) )
7 6 ineq2d 
 |-  ( ( A e. CH /\ B e. CH ) -> ( C i^i ( A vH B ) ) = ( C i^i ( B vH A ) ) )
8 7 3adant3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( C i^i ( A vH B ) ) = ( C i^i ( B vH A ) ) )
9 df-ss 
 |-  ( C C_ ( A vH B ) <-> ( C i^i ( A vH B ) ) = C )
10 9 biimpi 
 |-  ( C C_ ( A vH B ) -> ( C i^i ( A vH B ) ) = C )
11 8 10 sylan9req 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ C C_ ( A vH B ) ) -> ( C i^i ( B vH A ) ) = C )
12 11 3ad2antr3 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( C i^i ( B vH A ) ) = C )
13 5 12 eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C /\ C C_ ( A vH B ) ) ) -> ( ( C i^i B ) vH A ) = C )