Metamath Proof Explorer

Theorem dmdi

Description: Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dmdbr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )
2 1 biimpd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B -> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )
3 sseq2 
 |-  ( x = C -> ( B C_ x <-> B C_ C ) )
4 ineq1 
 |-  ( x = C -> ( x i^i A ) = ( C i^i A ) )
5 4 oveq1d 
 |-  ( x = C -> ( ( x i^i A ) vH B ) = ( ( C i^i A ) vH B ) )
6 ineq1 
 |-  ( x = C -> ( x i^i ( A vH B ) ) = ( C i^i ( A vH B ) ) )
7 5 6 eqeq12d 
 |-  ( x = C -> ( ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) <-> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) ) )
8 3 7 imbi12d 
 |-  ( x = C -> ( ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) <-> ( B C_ C -> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) ) ) )
9 8 rspcv 
 |-  ( C e. CH -> ( A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) -> ( B C_ C -> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) ) ) )
10 2 9 sylan9 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ C e. CH ) -> ( A MH* B -> ( B C_ C -> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) ) ) )
11 10 3impa 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A MH* B -> ( B C_ C -> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) ) ) )
12 11 imp32 
 |-  ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A MH* B /\ B C_ C ) ) -> ( ( C i^i A ) vH B ) = ( C i^i ( A vH B ) ) )