Metamath Proof Explorer

Theorem mddmdin0i

Description: If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of Holland p. 1524 to hold. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mddmdin0.1 
|- A e. CH
mddmdin0.2 
|- B e. CH
mddmdin0.3 
|- A. x e. CH A. y e. CH ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y )
Assertion mddmdin0i 
|- ( A MH* B -> A MH B )

Proof

Step Hyp Ref Expression
1 mddmdin0.1 
 |-  A e. CH
2 mddmdin0.2 
 |-  B e. CH
3 mddmdin0.3 
 |-  A. x e. CH A. y e. CH ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y )
4 inindir 
 |-  ( ( A i^i B ) i^i ( _|_ ` ( A i^i B ) ) ) = ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) )
5 1 2 chincli 
 |-  ( A i^i B ) e. CH
6 5 chocini 
 |-  ( ( A i^i B ) i^i ( _|_ ` ( A i^i B ) ) ) = 0H
7 4 6 eqtr3i 
 |-  ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H
8 5 choccli 
 |-  ( _|_ ` ( A i^i B ) ) e. CH
9 1 8 chincli 
 |-  ( A i^i ( _|_ ` ( A i^i B ) ) ) e. CH
10 2 8 chincli 
 |-  ( B i^i ( _|_ ` ( A i^i B ) ) ) e. CH
11 breq1 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( x MH* y <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y ) )
12 ineq1 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( x i^i y ) = ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) )
13 12 eqeq1d 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( x i^i y ) = 0H <-> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H ) )
14 11 13 anbi12d 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( x MH* y /\ ( x i^i y ) = 0H ) <-> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H ) ) )
15 breq1 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( x MH y <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH y ) )
16 14 15 imbi12d 
 |-  ( x = ( A i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y ) <-> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH y ) ) )
17 breq2 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) ) )
18 ineq2 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) )
19 18 eqeq1d 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H <-> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) )
20 17 19 anbi12d 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H ) <-> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) ) )
21 breq2 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH y <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) ) )
22 20 21 imbi12d 
 |-  ( y = ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* y /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i y ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH y ) <-> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) ) ) )
23 16 22 rspc2v 
 |-  ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) e. CH /\ ( B i^i ( _|_ ` ( A i^i B ) ) ) e. CH ) -> ( A. x e. CH A. y e. CH ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y ) -> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) ) ) )
24 9 10 23 mp2an 
 |-  ( A. x e. CH A. y e. CH ( ( x MH* y /\ ( x i^i y ) = 0H ) -> x MH y ) -> ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) ) )
25 3 24 ax-mp 
 |-  ( ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) /\ ( ( A i^i ( _|_ ` ( A i^i B ) ) ) i^i ( B i^i ( _|_ ` ( A i^i B ) ) ) ) = 0H ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) )
26 7 25 mpan2 
 |-  ( ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) -> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) )
27 1 2 dmdcompli 
 |-  ( A MH* B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH* ( B i^i ( _|_ ` ( A i^i B ) ) ) )
28 1 2 mdcompli 
 |-  ( A MH B <-> ( A i^i ( _|_ ` ( A i^i B ) ) ) MH ( B i^i ( _|_ ` ( A i^i B ) ) ) )
29 26 27 28 3imtr4i 
 |-  ( A MH* B -> A MH B )