Step |
Hyp |
Ref |
Expression |
1 |
|
mndcl.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
mndcl.p |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
mnd4g.1 |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
4 |
|
mnd4g.2 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
5 |
|
mnd4g.3 |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
6 |
|
mnd4g.4 |
⊢ ( 𝜑 → 𝑍 ∈ 𝐵 ) |
7 |
|
mnd4g.5 |
⊢ ( 𝜑 → 𝑊 ∈ 𝐵 ) |
8 |
|
mnd4g.6 |
⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) = ( 𝑍 + 𝑌 ) ) |
9 |
1 2 3 5 6 7 8
|
mnd12g |
⊢ ( 𝜑 → ( 𝑌 + ( 𝑍 + 𝑊 ) ) = ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) |
10 |
9
|
oveq2d |
⊢ ( 𝜑 → ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) ) |
11 |
1 2
|
mndcl |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑍 + 𝑊 ) ∈ 𝐵 ) |
12 |
3 6 7 11
|
syl3anc |
⊢ ( 𝜑 → ( 𝑍 + 𝑊 ) ∈ 𝐵 ) |
13 |
1 2
|
mndass |
⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑍 + 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) ) |
14 |
3 4 5 12 13
|
syl13anc |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( 𝑋 + ( 𝑌 + ( 𝑍 + 𝑊 ) ) ) ) |
15 |
1 2
|
mndcl |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 + 𝑊 ) ∈ 𝐵 ) |
16 |
3 5 7 15
|
syl3anc |
⊢ ( 𝜑 → ( 𝑌 + 𝑊 ) ∈ 𝐵 ) |
17 |
1 2
|
mndass |
⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑌 + 𝑊 ) ∈ 𝐵 ) ) → ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) ) |
18 |
3 4 6 16 17
|
syl13anc |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) = ( 𝑋 + ( 𝑍 + ( 𝑌 + 𝑊 ) ) ) ) |
19 |
10 14 18
|
3eqtr4d |
⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + ( 𝑍 + 𝑊 ) ) = ( ( 𝑋 + 𝑍 ) + ( 𝑌 + 𝑊 ) ) ) |