Step |
Hyp |
Ref |
Expression |
1 |
|
dihmeetlem5.b |
|- B = ( Base ` K ) |
2 |
|
dihmeetlem5.l |
|- .<_ = ( le ` K ) |
3 |
|
dihmeetlem5.j |
|- .\/ = ( join ` K ) |
4 |
|
dihmeetlem5.m |
|- ./\ = ( meet ` K ) |
5 |
|
dihmeetlem5.a |
|- A = ( Atoms ` K ) |
6 |
|
simpl1 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> K e. HL ) |
7 |
|
simprl |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Q e. A ) |
8 |
|
simpl2 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> X e. B ) |
9 |
|
simpl3 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Y e. B ) |
10 |
|
simprr |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> Q .<_ X ) |
11 |
1 2 3 4 5
|
atmod2i1 |
|- ( ( K e. HL /\ ( Q e. A /\ X e. B /\ Y e. B ) /\ Q .<_ X ) -> ( ( X ./\ Y ) .\/ Q ) = ( X ./\ ( Y .\/ Q ) ) ) |
12 |
6 7 8 9 10 11
|
syl131anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( ( X ./\ Y ) .\/ Q ) = ( X ./\ ( Y .\/ Q ) ) ) |
13 |
12
|
eqcomd |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Q e. A /\ Q .<_ X ) ) -> ( X ./\ ( Y .\/ Q ) ) = ( ( X ./\ Y ) .\/ Q ) ) |