Step |
Hyp |
Ref |
Expression |
1 |
|
omllaw3.b |
|- B = ( Base ` K ) |
2 |
|
omllaw3.l |
|- .<_ = ( le ` K ) |
3 |
|
omllaw3.m |
|- ./\ = ( meet ` K ) |
4 |
|
omllaw3.o |
|- ._|_ = ( oc ` K ) |
5 |
|
omllaw3.z |
|- .0. = ( 0. ` K ) |
6 |
|
oveq2 |
|- ( ( Y ./\ ( ._|_ ` X ) ) = .0. -> ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) = ( X ( join ` K ) .0. ) ) |
7 |
6
|
adantl |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) -> ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) = ( X ( join ` K ) .0. ) ) |
8 |
|
omlol |
|- ( K e. OML -> K e. OL ) |
9 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
10 |
1 9 5
|
olj01 |
|- ( ( K e. OL /\ X e. B ) -> ( X ( join ` K ) .0. ) = X ) |
11 |
8 10
|
sylan |
|- ( ( K e. OML /\ X e. B ) -> ( X ( join ` K ) .0. ) = X ) |
12 |
11
|
3adant3 |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X ( join ` K ) .0. ) = X ) |
13 |
12
|
adantr |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) -> ( X ( join ` K ) .0. ) = X ) |
14 |
7 13
|
eqtr2d |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) -> X = ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) ) |
15 |
14
|
adantrl |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X .<_ Y /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) ) -> X = ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) ) |
16 |
1 2 9 3 4
|
omllaw |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> Y = ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) ) ) |
17 |
16
|
imp |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ X .<_ Y ) -> Y = ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) ) |
18 |
17
|
adantrr |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X .<_ Y /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) ) -> Y = ( X ( join ` K ) ( Y ./\ ( ._|_ ` X ) ) ) ) |
19 |
15 18
|
eqtr4d |
|- ( ( ( K e. OML /\ X e. B /\ Y e. B ) /\ ( X .<_ Y /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) ) -> X = Y ) |
20 |
19
|
ex |
|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( ( X .<_ Y /\ ( Y ./\ ( ._|_ ` X ) ) = .0. ) -> X = Y ) ) |