Step |
Hyp |
Ref |
Expression |
1 |
|
gsumz.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
3 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
4 |
|
eqid |
⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } |
5 |
|
simpl |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → 𝐺 ∈ Mnd ) |
6 |
|
simpr |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 ) |
7 |
1
|
fvexi |
⊢ 0 ∈ V |
8 |
7
|
snid |
⊢ 0 ∈ { 0 } |
9 |
2 1 3 4
|
gsumvallem2 |
⊢ ( 𝐺 ∈ Mnd → { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } = { 0 } ) |
10 |
8 9
|
eleqtrrid |
⊢ ( 𝐺 ∈ Mnd → 0 ∈ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } ) |
11 |
10
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } ) |
12 |
11
|
fmpttd |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝑘 ∈ 𝐴 ↦ 0 ) : 𝐴 ⟶ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } ) |
13 |
2 1 3 4 5 6 12
|
gsumval1 |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 0 ) ) = 0 ) |