Metamath Proof Explorer

Theorem tnglem

Description: Lemma for tngbas and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses tngbas.t 
|- T = ( G toNrmGrp N )
tnglem.e 
|- E = Slot ( E ` ndx )
tnglem.t 
|- ( E ` ndx ) =/= ( TopSet ` ndx )
tnglem.d 
|- ( E ` ndx ) =/= ( dist ` ndx )
Assertion tnglem 
|- ( N e. V -> ( E ` G ) = ( E ` T ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 
 |-  T = ( G toNrmGrp N )
2 tnglem.e 
 |-  E = Slot ( E ` ndx )
3 tnglem.t 
 |-  ( E ` ndx ) =/= ( TopSet ` ndx )
4 tnglem.d 
 |-  ( E ` ndx ) =/= ( dist ` ndx )
5 2 4 setsnid 
 |-  ( E ` G ) = ( E ` ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) )
6 2 3 setsnid 
 |-  ( E ` ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
7 5 6 eqtri 
 |-  ( E ` G ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
8 eqid 
 |-  ( -g ` G ) = ( -g ` G )
9 eqid 
 |-  ( N o. ( -g ` G ) ) = ( N o. ( -g ` G ) )
10 eqid 
 |-  ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( MetOpen ` ( N o. ( -g ` G ) ) )
11 1 8 9 10 tngval 
 |-  ( ( G e. _V /\ N e. V ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
12 11 fveq2d 
 |-  ( ( G e. _V /\ N e. V ) -> ( E ` T ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) ) )
13 7 12 eqtr4id 
 |-  ( ( G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) )
14 2 str0 
 |-  (/) = ( E ` (/) )
15 14 eqcomi 
 |-  ( E ` (/) ) = (/)
16 reldmtng 
 |-  Rel dom toNrmGrp
17 15 1 16 oveqprc 
 |-  ( -. G e. _V -> ( E ` G ) = ( E ` T ) )
18 17 adantr 
 |-  ( ( -. G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) )
19 13 18 pm2.61ian 
 |-  ( N e. V -> ( E ` G ) = ( E ` T ) )