Step |
Hyp |
Ref |
Expression |
1 |
|
tngbas.t |
⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 ) |
2 |
|
tngsca.2 |
⊢ 𝐹 = ( Scalar ‘ 𝐺 ) |
3 |
|
scaid |
⊢ Scalar = Slot ( Scalar ‘ ndx ) |
4 |
|
slotstnscsi |
⊢ ( ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ) |
5 |
4
|
simp1i |
⊢ ( TopSet ‘ ndx ) ≠ ( Scalar ‘ ndx ) |
6 |
5
|
necomi |
⊢ ( Scalar ‘ ndx ) ≠ ( TopSet ‘ ndx ) |
7 |
|
slotsdnscsi |
⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ) |
8 |
7
|
simp1i |
⊢ ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) |
9 |
8
|
necomi |
⊢ ( Scalar ‘ ndx ) ≠ ( dist ‘ ndx ) |
10 |
1 3 6 9
|
tnglem |
⊢ ( 𝑁 ∈ 𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) ) |
11 |
2 10
|
eqtrid |
⊢ ( 𝑁 ∈ 𝑉 → 𝐹 = ( Scalar ‘ 𝑇 ) ) |