Metamath Proof Explorer

Theorem omllaw2N

Description: Variation of orthomodular law. Definition of OML law in Kalmbach p. 22. ( pjoml2i analog.) (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 omllaw.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omllaw.l ⊢ ≤ = ( le ‘ 𝐾 )
3 omllaw.j ⊢ ∨ = ( join ‘ 𝐾 )
4 omllaw.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 omllaw.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 1 2 3 4 5 omllaw ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
7 eqcom ⊢ ( ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) = 𝑌 ↔ 𝑌 = ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) )
8 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
10 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
11 1 5 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
12 10 11 sylan ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
13 12 3adant3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
14 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
15 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) = ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) )
16 9 13 14 15 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) = ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) )
17 16 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
18 17 eqeq2d ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 = ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) ↔ 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
19 7 18 bitrid ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) = 𝑌 ↔ 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
20 6 19 sylibrd ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ 𝑌 ) ) = 𝑌 ) )