Metamath Proof Explorer

Theorem omlmod1i2N

Description: Analogue of modular law atmod1i2 that holds in any OML. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses omlmod.b 
|- B = ( Base ` K )
omlmod.l 
|- .<_ = ( le ` K )
omlmod.j 
|- .\/ = ( join ` K )
omlmod.m 
|- ./\ = ( meet ` K )
omlmod.c 
|- C = ( cm ` K )
Assertion omlmod1i2N 
|- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ Z ) )

Proof

Step Hyp Ref Expression
1 omlmod.b 
 |-  B = ( Base ` K )
2 omlmod.l 
 |-  .<_ = ( le ` K )
3 omlmod.j 
 |-  .\/ = ( join ` K )
4 omlmod.m 
 |-  ./\ = ( meet ` K )
5 omlmod.c 
 |-  C = ( cm ` K )
6 simp1 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> K e. OML )
7 simp23 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> Z e. B )
8 simp21 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> X e. B )
9 simp22 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> Y e. B )
10 simp3l 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> X .<_ Z )
11 1 2 5 lecmtN 
 |-  ( ( K e. OML /\ X e. B /\ Z e. B ) -> ( X .<_ Z -> X C Z ) )
12 6 8 7 11 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .<_ Z -> X C Z ) )
13 10 12 mpd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> X C Z )
14 1 5 cmtcomN 
 |-  ( ( K e. OML /\ X e. B /\ Z e. B ) -> ( X C Z <-> Z C X ) )
15 6 8 7 14 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X C Z <-> Z C X ) )
16 13 15 mpbid 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> Z C X )
17 simp3r 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> Y C Z )
18 1 5 cmtcomN 
 |-  ( ( K e. OML /\ Y e. B /\ Z e. B ) -> ( Y C Z <-> Z C Y ) )
19 6 9 7 18 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( Y C Z <-> Z C Y ) )
20 17 19 mpbid 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> Z C Y )
21 1 3 4 5 omlfh1N 
 |-  ( ( K e. OML /\ ( Z e. B /\ X e. B /\ Y e. B ) /\ ( Z C X /\ Z C Y ) ) -> ( Z ./\ ( X .\/ Y ) ) = ( ( Z ./\ X ) .\/ ( Z ./\ Y ) ) )
22 6 7 8 9 16 20 21 syl132anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( Z ./\ ( X .\/ Y ) ) = ( ( Z ./\ X ) .\/ ( Z ./\ Y ) ) )
23 omllat 
 |-  ( K e. OML -> K e. Lat )
24 23 3ad2ant1 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> K e. Lat )
25 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B )
26 24 8 9 25 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .\/ Y ) e. B )
27 1 4 latmcom 
 |-  ( ( K e. Lat /\ Z e. B /\ ( X .\/ Y ) e. B ) -> ( Z ./\ ( X .\/ Y ) ) = ( ( X .\/ Y ) ./\ Z ) )
28 24 7 26 27 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( Z ./\ ( X .\/ Y ) ) = ( ( X .\/ Y ) ./\ Z ) )
29 1 2 4 latleeqm2 
 |-  ( ( K e. Lat /\ X e. B /\ Z e. B ) -> ( X .<_ Z <-> ( Z ./\ X ) = X ) )
30 24 8 7 29 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .<_ Z <-> ( Z ./\ X ) = X ) )
31 10 30 mpbid 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( Z ./\ X ) = X )
32 1 4 latmcom 
 |-  ( ( K e. Lat /\ Z e. B /\ Y e. B ) -> ( Z ./\ Y ) = ( Y ./\ Z ) )
33 24 7 9 32 syl3anc 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( Z ./\ Y ) = ( Y ./\ Z ) )
34 31 33 oveq12d 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( ( Z ./\ X ) .\/ ( Z ./\ Y ) ) = ( X .\/ ( Y ./\ Z ) ) )
35 22 28 34 3eqtr3rd 
 |-  ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ Z ) )