Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tnglem Structured version   Visualization version   Unicode version

Theorem tnglem 21726
 Description: Lemma for tngbas 21727 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
tngbas.t toNrmGrp
tnglem.2 Slot
tnglem.3
tnglem.4
Assertion
Ref Expression
tnglem

Proof of Theorem tnglem
StepHypRef Expression
1 tngbas.t . . . . 5 toNrmGrp
2 eqid 2471 . . . . 5
3 eqid 2471 . . . . 5
4 eqid 2471 . . . . 5
51, 2, 3, 4tngval 21725 . . . 4 sSet sSet TopSet
65fveq2d 5883 . . 3 sSet sSet TopSet
7 tnglem.2 . . . . . 6 Slot
8 tnglem.3 . . . . . 6
97, 8ndxid 15220 . . . . 5 Slot
107, 8ndxarg 15219 . . . . . . . 8
118nnrei 10640 . . . . . . . 8
1210, 11eqeltri 2545 . . . . . . 7
13 tnglem.4 . . . . . . . . 9
1410, 13eqbrtri 4415 . . . . . . . 8
15 1nn 10642 . . . . . . . . 9
16 2nn0 10910 . . . . . . . . 9
17 9nn0 10917 . . . . . . . . 9
18 9lt10 10835 . . . . . . . . 9
1915, 16, 17, 18declti 11099 . . . . . . . 8 ;
20 9re 10718 . . . . . . . . 9
21 1nn0 10909 . . . . . . . . . . 11
2221, 16deccl 11088 . . . . . . . . . 10 ;
2322nn0rei 10904 . . . . . . . . 9 ;
2412, 20, 23lttri 9778 . . . . . . . 8 ; ;
2514, 19, 24mp2an 686 . . . . . . 7 ;
2612, 25ltneii 9765 . . . . . 6 ;
27 dsndx 15378 . . . . . 6 ;
2826, 27neeqtrri 2716 . . . . 5
299, 28setsnid 15243 . . . 4 sSet
3012, 14ltneii 9765 . . . . . 6
31 tsetndx 15362 . . . . . 6 TopSet
3230, 31neeqtrri 2716 . . . . 5 TopSet
339, 32setsnid 15243 . . . 4 sSet sSet sSet TopSet
3429, 33eqtri 2493 . . 3 sSet sSet TopSet
356, 34syl6reqr 2524 . 2
367str0 15239 . . 3
37 fvprc 5873 . . . 4