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

Metamath Proof Explorer

Theorem mdsl3

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

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

Proof

Step Hyp Ref Expression
1 mdi 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) )
2 1 3adantr2 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = ( C vH ( A i^i B ) ) )
3 chincl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
4 chlejb2 
 |-  ( ( ( A i^i B ) e. CH /\ C e. CH ) -> ( ( A i^i B ) C_ C <-> ( C vH ( A i^i B ) ) = C ) )
5 3 4 stoic3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A i^i B ) C_ C <-> ( C vH ( A i^i B ) ) = C ) )
6 5 biimpa 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A i^i B ) C_ C ) -> ( C vH ( A i^i B ) ) = C )
7 6 3ad2antr2 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( C vH ( A i^i B ) ) = C )
8 2 7 eqtrd 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH B /\ ( A i^i B ) C_ C /\ C C_ B ) ) -> ( ( C vH A ) i^i B ) = C )