Metamath Proof Explorer


Theorem isoml

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

Ref Expression
Hypotheses isoml.b B=BaseK
isoml.l ˙=K
isoml.j ˙=joinK
isoml.m ˙=meetK
isoml.o ˙=ocK
Assertion isoml KOMLKOLxByBx˙yy=x˙y˙˙x

Proof

Step Hyp Ref Expression
1 isoml.b B=BaseK
2 isoml.l ˙=K
3 isoml.j ˙=joinK
4 isoml.m ˙=meetK
5 isoml.o ˙=ocK
6 fveq2 k=KBasek=BaseK
7 6 1 eqtr4di k=KBasek=B
8 fveq2 k=Kk=K
9 8 2 eqtr4di k=Kk=˙
10 9 breqd k=Kxkyx˙y
11 fveq2 k=Kjoink=joinK
12 11 3 eqtr4di k=Kjoink=˙
13 eqidd k=Kx=x
14 fveq2 k=Kmeetk=meetK
15 14 4 eqtr4di k=Kmeetk=˙
16 eqidd k=Ky=y
17 fveq2 k=Kock=ocK
18 17 5 eqtr4di k=Kock=˙
19 18 fveq1d k=Kockx=˙x
20 15 16 19 oveq123d k=Kymeetkockx=y˙˙x
21 12 13 20 oveq123d k=Kxjoinkymeetkockx=x˙y˙˙x
22 21 eqeq2d k=Ky=xjoinkymeetkockxy=x˙y˙˙x
23 10 22 imbi12d k=Kxkyy=xjoinkymeetkockxx˙yy=x˙y˙˙x
24 7 23 raleqbidv k=KyBasekxkyy=xjoinkymeetkockxyBx˙yy=x˙y˙˙x
25 7 24 raleqbidv k=KxBasekyBasekxkyy=xjoinkymeetkockxxByBx˙yy=x˙y˙˙x
26 df-oml OML=kOL|xBasekyBasekxkyy=xjoinkymeetkockx
27 25 26 elrab2 KOMLKOLxByBx˙yy=x˙y˙˙x