Step |
Hyp |
Ref |
Expression |
1 |
|
tngbas.t |
|- T = ( G toNrmGrp N ) |
2 |
|
tngsca.2 |
|- F = ( Scalar ` G ) |
3 |
|
scaid |
|- Scalar = Slot ( Scalar ` ndx ) |
4 |
|
slotstnscsi |
|- ( ( TopSet ` ndx ) =/= ( Scalar ` ndx ) /\ ( TopSet ` ndx ) =/= ( .s ` ndx ) /\ ( TopSet ` ndx ) =/= ( .i ` ndx ) ) |
5 |
4
|
simp1i |
|- ( TopSet ` ndx ) =/= ( Scalar ` ndx ) |
6 |
5
|
necomi |
|- ( Scalar ` ndx ) =/= ( TopSet ` ndx ) |
7 |
|
slotsdnscsi |
|- ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) ) |
8 |
7
|
simp1i |
|- ( dist ` ndx ) =/= ( Scalar ` ndx ) |
9 |
8
|
necomi |
|- ( Scalar ` ndx ) =/= ( dist ` ndx ) |
10 |
1 3 6 9
|
tnglem |
|- ( N e. V -> ( Scalar ` G ) = ( Scalar ` T ) ) |
11 |
2 10
|
eqtrid |
|- ( N e. V -> F = ( Scalar ` T ) ) |