This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omllaw5N

Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses omllaw5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
omllaw5.j ⊢ ∨ = ( join ‘ 𝐾 )
omllaw5.m ⊢ ∧ = ( meet ‘ 𝐾 )
omllaw5.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion omllaw5N ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 omllaw5.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omllaw5.j ⊢ ∨ = ( join ‘ 𝐾 )
3 omllaw5.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 omllaw5.o ⊢ ⊥ = ( oc ‘ 𝐾 )
5 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML )
6 simp2 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
8 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
9 7 8 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
10 5 6 9 3jca ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
13 7 12 syl3an1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
14 1 11 2 3 4 omllaw2N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) ) )
15 10 13 14 sylc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )