Step |
Hyp |
Ref |
Expression |
1 |
|
tgpsubcn.2 |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
2 |
|
tgpsubcn.3 |
⊢ − = ( -g ‘ 𝐺 ) |
3 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
4 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
5 |
|
eqid |
⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 ) |
6 |
3 4 5 2
|
grpsubfval |
⊢ − = ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) |
7 |
|
tgptmd |
⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd ) |
8 |
1 3
|
tgptopon |
⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
9 |
8 8
|
cnmpt1st |
⊢ ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
10 |
8 8
|
cnmpt2nd |
⊢ ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
11 |
1 5
|
tgpinv |
⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Cn 𝐽 ) ) |
12 |
8 8 10 11
|
cnmpt21f |
⊢ ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
13 |
1 4 7 8 8 9 12
|
cnmpt2plusg |
⊢ ( 𝐺 ∈ TopGrp → ( 𝑥 ∈ ( Base ‘ 𝐺 ) , 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |
14 |
6 13
|
eqeltrid |
⊢ ( 𝐺 ∈ TopGrp → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) |