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 𝐵 = ( Base ‘ 𝐾 )
omlmod.l = ( le ‘ 𝐾 )
omlmod.j = ( join ‘ 𝐾 )
omlmod.m = ( meet ‘ 𝐾 )
omlmod.c 𝐶 = ( cm ‘ 𝐾 )
Assertion omlmod1i2N ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 ( 𝑌 𝑍 ) ) = ( ( 𝑋 𝑌 ) 𝑍 ) )

Proof

Step Hyp Ref Expression
1 omlmod.b 𝐵 = ( Base ‘ 𝐾 )
2 omlmod.l = ( le ‘ 𝐾 )
3 omlmod.j = ( join ‘ 𝐾 )
4 omlmod.m = ( meet ‘ 𝐾 )
5 omlmod.c 𝐶 = ( cm ‘ 𝐾 )
6 simp1 ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ OML )
7 simp23 ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑍𝐵 )
8 simp21 ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑋𝐵 )
9 simp22 ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑌𝐵 )
10 simp3l ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑋 𝑍 )
11 1 2 5 lecmtN ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵 ) → ( 𝑋 𝑍𝑋 𝐶 𝑍 ) )
12 6 8 7 11 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 𝑍𝑋 𝐶 𝑍 ) )
13 10 12 mpd ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑋 𝐶 𝑍 )
14 1 5 cmtcomN ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵 ) → ( 𝑋 𝐶 𝑍𝑍 𝐶 𝑋 ) )
15 6 8 7 14 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 𝐶 𝑍𝑍 𝐶 𝑋 ) )
16 13 15 mpbid ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑍 𝐶 𝑋 )
17 simp3r ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑌 𝐶 𝑍 )
18 1 5 cmtcomN ( ( 𝐾 ∈ OML ∧ 𝑌𝐵𝑍𝐵 ) → ( 𝑌 𝐶 𝑍𝑍 𝐶 𝑌 ) )
19 6 9 7 18 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑌 𝐶 𝑍𝑍 𝐶 𝑌 ) )
20 17 19 mpbid ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝑍 𝐶 𝑌 )
21 1 3 4 5 omlfh1N ( ( 𝐾 ∈ OML ∧ ( 𝑍𝐵𝑋𝐵𝑌𝐵 ) ∧ ( 𝑍 𝐶 𝑋𝑍 𝐶 𝑌 ) ) → ( 𝑍 ( 𝑋 𝑌 ) ) = ( ( 𝑍 𝑋 ) ( 𝑍 𝑌 ) ) )
22 6 7 8 9 16 20 21 syl132anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑍 ( 𝑋 𝑌 ) ) = ( ( 𝑍 𝑋 ) ( 𝑍 𝑌 ) ) )
23 omllat ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
24 23 3ad2ant1 ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ Lat )
25 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
26 24 8 9 25 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 𝑌 ) ∈ 𝐵 )
27 1 4 latmcom ( ( 𝐾 ∈ Lat ∧ 𝑍𝐵 ∧ ( 𝑋 𝑌 ) ∈ 𝐵 ) → ( 𝑍 ( 𝑋 𝑌 ) ) = ( ( 𝑋 𝑌 ) 𝑍 ) )
28 24 7 26 27 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑍 ( 𝑋 𝑌 ) ) = ( ( 𝑋 𝑌 ) 𝑍 ) )
29 1 2 4 latleeqm2 ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑍𝐵 ) → ( 𝑋 𝑍 ↔ ( 𝑍 𝑋 ) = 𝑋 ) )
30 24 8 7 29 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 𝑍 ↔ ( 𝑍 𝑋 ) = 𝑋 ) )
31 10 30 mpbid ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑍 𝑋 ) = 𝑋 )
32 1 4 latmcom ( ( 𝐾 ∈ Lat ∧ 𝑍𝐵𝑌𝐵 ) → ( 𝑍 𝑌 ) = ( 𝑌 𝑍 ) )
33 24 7 9 32 syl3anc ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑍 𝑌 ) = ( 𝑌 𝑍 ) )
34 31 33 oveq12d ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( ( 𝑍 𝑋 ) ( 𝑍 𝑌 ) ) = ( 𝑋 ( 𝑌 𝑍 ) ) )
35 22 28 34 3eqtr3rd ( ( 𝐾 ∈ OML ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ∧ ( 𝑋 𝑍𝑌 𝐶 𝑍 ) ) → ( 𝑋 ( 𝑌 𝑍 ) ) = ( ( 𝑋 𝑌 ) 𝑍 ) )