# 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 )`
` |-  ( ( 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 ) )`