Step |
Hyp |
Ref |
Expression |
1 |
|
ngprcan.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
ngprcan.p |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
ngprcan.d |
⊢ 𝐷 = ( dist ‘ 𝐺 ) |
4 |
|
simplr |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ Abel ) |
5 |
|
simpr3 |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐶 ∈ 𝑋 ) |
6 |
|
simpr1 |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
7 |
1 2
|
ablcom |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 + 𝐴 ) = ( 𝐴 + 𝐶 ) ) |
8 |
4 5 6 7
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 + 𝐴 ) = ( 𝐴 + 𝐶 ) ) |
9 |
|
simpr2 |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
10 |
1 2
|
ablcom |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) ) |
11 |
4 5 9 10
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) ) |
12 |
8 11
|
oveq12d |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 + 𝐴 ) 𝐷 ( 𝐶 + 𝐵 ) ) = ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) ) |
13 |
1 2 3
|
ngprcan |
⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) ) |
14 |
13
|
adantlr |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐶 ) 𝐷 ( 𝐵 + 𝐶 ) ) = ( 𝐴 𝐷 𝐵 ) ) |
15 |
12 14
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ NrmGrp ∧ 𝐺 ∈ Abel ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐶 + 𝐴 ) 𝐷 ( 𝐶 + 𝐵 ) ) = ( 𝐴 𝐷 𝐵 ) ) |