Metamath Proof Explorer


Definition df-oml

Description: Define the class of orthomodular lattices. Definition from Kalmbach p. 16. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion df-oml OML = { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 coml OML
1 vl 𝑙
2 col OL
3 va 𝑎
4 cbs Base
5 1 cv 𝑙
6 5 4 cfv ( Base ‘ 𝑙 )
7 vb 𝑏
8 3 cv 𝑎
9 cple le
10 5 9 cfv ( le ‘ 𝑙 )
11 7 cv 𝑏
12 8 11 10 wbr 𝑎 ( le ‘ 𝑙 ) 𝑏
13 cjn join
14 5 13 cfv ( join ‘ 𝑙 )
15 cmee meet
16 5 15 cfv ( meet ‘ 𝑙 )
17 coc oc
18 5 17 cfv ( oc ‘ 𝑙 )
19 8 18 cfv ( ( oc ‘ 𝑙 ) ‘ 𝑎 )
20 11 19 16 co ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) )
21 8 20 14 co ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) )
22 11 21 wceq 𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) )
23 12 22 wi ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
24 23 7 6 wral 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
25 24 3 6 wral 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) )
26 25 1 2 crab { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }
27 0 26 wceq OML = { 𝑙 ∈ OL ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑙 ) ∀ 𝑏 ∈ ( Base ‘ 𝑙 ) ( 𝑎 ( le ‘ 𝑙 ) 𝑏𝑏 = ( 𝑎 ( join ‘ 𝑙 ) ( 𝑏 ( meet ‘ 𝑙 ) ( ( oc ‘ 𝑙 ) ‘ 𝑎 ) ) ) ) }