Metamath Proof Explorer

Theorem isoml

Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses isoml.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isoml.l ⊢ ≤ = ( le ‘ 𝐾 )
isoml.j ⊢ ∨ = ( join ‘ 𝐾 )
isoml.m ⊢ ∧ = ( meet ‘ 𝐾 )
isoml.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion isoml ( 𝐾 ∈ OML ↔ ( 𝐾 ∈ OL ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isoml.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isoml.l ⊢ ≤ = ( le ‘ 𝐾 )
3 isoml.j ⊢ ∨ = ( join ‘ 𝐾 )
4 isoml.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 isoml.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
7 6 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
9 8 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
10 9 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
11 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
12 11 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
13 eqidd ⊢ ( 𝑘 = 𝐾 → 𝑥 = 𝑥 )
14 fveq2 ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ( meet ‘ 𝐾 ) )
15 14 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( meet ‘ 𝑘 ) = ∧ )
16 eqidd ⊢ ( 𝑘 = 𝐾 → 𝑦 = 𝑦 )
17 fveq2 ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ( oc ‘ 𝐾 ) )
18 17 5 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( oc ‘ 𝑘 ) = ⊥ )
19 18 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) = ( ⊥ ‘ 𝑥 ) )
20 15 16 19 oveq123d ⊢ ( 𝑘 = 𝐾 → ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) = ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) )
21 12 13 20 oveq123d ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) )
22 21 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑦 = ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) ↔ 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) )
23 10 22 imbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ( le ‘ 𝑘 ) 𝑦 → 𝑦 = ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ↔ ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )
24 7 23 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 → 𝑦 = ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )
25 7 24 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 → 𝑦 = ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )
26 df-oml ⊢ OML = { 𝑘 ∈ OL ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 → 𝑦 = ( 𝑥 ( join ‘ 𝑘 ) ( 𝑦 ( meet ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) }
27 25 26 elrab2 ⊢ ( 𝐾 ∈ OML ↔ ( 𝐾 ∈ OL ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )