| Step |
Hyp |
Ref |
Expression |
| 1 |
|
latjass.b |
|- B = ( Base ` K ) |
| 2 |
|
latjass.j |
|- .\/ = ( join ` K ) |
| 3 |
|
simpl |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat ) |
| 4 |
|
simpr3 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B ) |
| 5 |
|
simpr1 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B ) |
| 6 |
|
simpr2 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B ) |
| 7 |
1 2
|
latj12 |
|- ( ( K e. Lat /\ ( Z e. B /\ X e. B /\ Y e. B ) ) -> ( Z .\/ ( X .\/ Y ) ) = ( X .\/ ( Z .\/ Y ) ) ) |
| 8 |
3 4 5 6 7
|
syl13anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z .\/ ( X .\/ Y ) ) = ( X .\/ ( Z .\/ Y ) ) ) |
| 9 |
1 2
|
latjcl |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B ) |
| 10 |
9
|
3adant3r3 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ Y ) e. B ) |
| 11 |
1 2
|
latjcom |
|- ( ( K e. Lat /\ ( X .\/ Y ) e. B /\ Z e. B ) -> ( ( X .\/ Y ) .\/ Z ) = ( Z .\/ ( X .\/ Y ) ) ) |
| 12 |
3 10 4 11
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( Z .\/ ( X .\/ Y ) ) ) |
| 13 |
1 2
|
latjcl |
|- ( ( K e. Lat /\ Z e. B /\ Y e. B ) -> ( Z .\/ Y ) e. B ) |
| 14 |
3 4 6 13
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z .\/ Y ) e. B ) |
| 15 |
1 2
|
latjcom |
|- ( ( K e. Lat /\ ( Z .\/ Y ) e. B /\ X e. B ) -> ( ( Z .\/ Y ) .\/ X ) = ( X .\/ ( Z .\/ Y ) ) ) |
| 16 |
3 14 5 15
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Z .\/ Y ) .\/ X ) = ( X .\/ ( Z .\/ Y ) ) ) |
| 17 |
8 12 16
|
3eqtr4d |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .\/ Y ) .\/ Z ) = ( ( Z .\/ Y ) .\/ X ) ) |