Step |
Hyp |
Ref |
Expression |
1 |
|
ablcom.b |
|- B = ( Base ` G ) |
2 |
|
ablcom.p |
|- .+ = ( +g ` G ) |
3 |
|
simp1 |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. CMnd ) |
4 |
|
cmnmnd |
|- ( G e. CMnd -> G e. Mnd ) |
5 |
3 4
|
syl |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> G e. Mnd ) |
6 |
|
simp2l |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> X e. B ) |
7 |
|
simp2r |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Y e. B ) |
8 |
|
simp3l |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> Z e. B ) |
9 |
|
simp3r |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> W e. B ) |
10 |
1 2
|
cmncom |
|- ( ( G e. CMnd /\ Y e. B /\ Z e. B ) -> ( Y .+ Z ) = ( Z .+ Y ) ) |
11 |
3 7 8 10
|
syl3anc |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( Y .+ Z ) = ( Z .+ Y ) ) |
12 |
1 2 5 6 7 8 9 11
|
mnd4g |
|- ( ( G e. CMnd /\ ( X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) ) |