Step |
Hyp |
Ref |
Expression |
1 |
|
mndcl.b |
|- B = ( Base ` G ) |
2 |
|
mndcl.p |
|- .+ = ( +g ` G ) |
3 |
|
mnd4g.1 |
|- ( ph -> G e. Mnd ) |
4 |
|
mnd4g.2 |
|- ( ph -> X e. B ) |
5 |
|
mnd4g.3 |
|- ( ph -> Y e. B ) |
6 |
|
mnd4g.4 |
|- ( ph -> Z e. B ) |
7 |
|
mnd4g.5 |
|- ( ph -> W e. B ) |
8 |
|
mnd4g.6 |
|- ( ph -> ( Y .+ Z ) = ( Z .+ Y ) ) |
9 |
1 2 3 5 6 7 8
|
mnd12g |
|- ( ph -> ( Y .+ ( Z .+ W ) ) = ( Z .+ ( Y .+ W ) ) ) |
10 |
9
|
oveq2d |
|- ( ph -> ( X .+ ( Y .+ ( Z .+ W ) ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
11 |
1 2
|
mndcl |
|- ( ( G e. Mnd /\ Z e. B /\ W e. B ) -> ( Z .+ W ) e. B ) |
12 |
3 6 7 11
|
syl3anc |
|- ( ph -> ( Z .+ W ) e. B ) |
13 |
1 2
|
mndass |
|- ( ( G e. Mnd /\ ( X e. B /\ Y e. B /\ ( Z .+ W ) e. B ) ) -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( X .+ ( Y .+ ( Z .+ W ) ) ) ) |
14 |
3 4 5 12 13
|
syl13anc |
|- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( X .+ ( Y .+ ( Z .+ W ) ) ) ) |
15 |
1 2
|
mndcl |
|- ( ( G e. Mnd /\ Y e. B /\ W e. B ) -> ( Y .+ W ) e. B ) |
16 |
3 5 7 15
|
syl3anc |
|- ( ph -> ( Y .+ W ) e. B ) |
17 |
1 2
|
mndass |
|- ( ( G e. Mnd /\ ( X e. B /\ Z e. B /\ ( Y .+ W ) e. B ) ) -> ( ( X .+ Z ) .+ ( Y .+ W ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
18 |
3 4 6 16 17
|
syl13anc |
|- ( ph -> ( ( X .+ Z ) .+ ( Y .+ W ) ) = ( X .+ ( Z .+ ( Y .+ W ) ) ) ) |
19 |
10 14 18
|
3eqtr4d |
|- ( ph -> ( ( X .+ Y ) .+ ( Z .+ W ) ) = ( ( X .+ Z ) .+ ( Y .+ W ) ) ) |