Step |
Hyp |
Ref |
Expression |
0 |
|
csg |
⊢ -g |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑔 ) |
7 |
|
vy |
⊢ 𝑦 |
8 |
3
|
cv |
⊢ 𝑥 |
9 |
|
cplusg |
⊢ +g |
10 |
5 9
|
cfv |
⊢ ( +g ‘ 𝑔 ) |
11 |
|
cminusg |
⊢ invg |
12 |
5 11
|
cfv |
⊢ ( invg ‘ 𝑔 ) |
13 |
7
|
cv |
⊢ 𝑦 |
14 |
13 12
|
cfv |
⊢ ( ( invg ‘ 𝑔 ) ‘ 𝑦 ) |
15 |
8 14 10
|
co |
⊢ ( 𝑥 ( +g ‘ 𝑔 ) ( ( invg ‘ 𝑔 ) ‘ 𝑦 ) ) |
16 |
3 7 6 6 15
|
cmpo |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) ( ( invg ‘ 𝑔 ) ‘ 𝑦 ) ) ) |
17 |
1 2 16
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) ( ( invg ‘ 𝑔 ) ‘ 𝑦 ) ) ) ) |
18 |
0 17
|
wceq |
⊢ -g = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) ( ( invg ‘ 𝑔 ) ‘ 𝑦 ) ) ) ) |