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 )