| 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 |
|
simpr2 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B ) |
| 5 |
|
simpr3 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B ) |
| 6 |
|
simpr1 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B ) |
| 7 |
1 2
|
latj32 |
|- ( ( K e. Lat /\ ( Y e. B /\ Z e. B /\ X e. B ) ) -> ( ( Y .\/ Z ) .\/ X ) = ( ( Y .\/ X ) .\/ Z ) ) |
| 8 |
3 4 5 6 7
|
syl13anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( Y .\/ Z ) .\/ X ) = ( ( Y .\/ X ) .\/ Z ) ) |
| 9 |
1 2
|
latjcl |
|- ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y .\/ Z ) e. B ) |
| 10 |
9
|
3adant3r1 |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ Z ) e. B ) |
| 11 |
1 2
|
latjcom |
|- ( ( K e. Lat /\ X e. B /\ ( Y .\/ Z ) e. B ) -> ( X .\/ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) .\/ X ) ) |
| 12 |
3 6 10 11
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( ( Y .\/ Z ) .\/ X ) ) |
| 13 |
1 2
|
latjcl |
|- ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .\/ X ) e. B ) |
| 14 |
3 4 6 13
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .\/ X ) e. B ) |
| 15 |
1 2
|
latjcom |
|- ( ( K e. Lat /\ Z e. B /\ ( Y .\/ X ) e. B ) -> ( Z .\/ ( Y .\/ X ) ) = ( ( Y .\/ X ) .\/ Z ) ) |
| 16 |
3 5 14 15
|
syl3anc |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z .\/ ( Y .\/ X ) ) = ( ( Y .\/ X ) .\/ Z ) ) |
| 17 |
8 12 16
|
3eqtr4d |
|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y .\/ Z ) ) = ( Z .\/ ( Y .\/ X ) ) ) |