Metamath Proof Explorer

Theorem tnglem

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

Ref Expression
Hypotheses tngbas.t 
|- T = ( G toNrmGrp N )
tnglem.2 
|- E = Slot K
tnglem.3 
|- K e. NN
tnglem.4 
|- K < 9
Assertion tnglem 
|- ( N e. V -> ( E ` G ) = ( E ` T ) )

Proof

Step Hyp Ref Expression
1 tngbas.t 
 |-  T = ( G toNrmGrp N )
2 tnglem.2 
 |-  E = Slot K
3 tnglem.3 
 |-  K e. NN
4 tnglem.4 
 |-  K < 9
5 2 3 ndxid 
 |-  E = Slot ( E ` ndx )
6 2 3 ndxarg 
 |-  ( E ` ndx ) = K
7 3 nnrei 
 |-  K e. RR
8 6 7 eqeltri 
 |-  ( E ` ndx ) e. RR
9 6 4 eqbrtri 
 |-  ( E ` ndx ) < 9
10 1nn 
 |-  1 e. NN
11 2nn0 
 |-  2 e. NN0
12 9nn0 
 |-  9 e. NN0
13 9lt10 
 |-  9 < ; 1 0
14 10 11 12 13 declti 
 |-  9 < ; 1 2
15 9re 
 |-  9 e. RR
16 1nn0 
 |-  1 e. NN0
17 16 11 deccl 
 |-  ; 1 2 e. NN0
18 17 nn0rei 
 |-  ; 1 2 e. RR
19 8 15 18 lttri 
 |-  ( ( ( E ` ndx ) < 9 /\ 9 < ; 1 2 ) -> ( E ` ndx ) < ; 1 2 )
20 9 14 19 mp2an 
 |-  ( E ` ndx ) < ; 1 2
21 8 20 ltneii 
 |-  ( E ` ndx ) =/= ; 1 2
22 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
23 21 22 neeqtrri 
 |-  ( E ` ndx ) =/= ( dist ` ndx )
24 5 23 setsnid 
 |-  ( E ` G ) = ( E ` ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) )
25 8 9 ltneii 
 |-  ( E ` ndx ) =/= 9
26 tsetndx 
 |-  ( TopSet ` ndx ) = 9
27 25 26 neeqtrri 
 |-  ( E ` ndx ) =/= ( TopSet ` ndx )
28 5 27 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 ) ) ) >. ) )
29 24 28 eqtri 
 |-  ( E ` G ) = ( E ` ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
30 eqid 
 |-  ( -g ` G ) = ( -g ` G )
31 eqid 
 |-  ( N o. ( -g ` G ) ) = ( N o. ( -g ` G ) )
32 eqid 
 |-  ( MetOpen ` ( N o. ( -g ` G ) ) ) = ( MetOpen ` ( N o. ( -g ` G ) ) )
33 1 30 31 32 tngval 
 |-  ( ( G e. _V /\ N e. V ) -> T = ( ( G sSet <. ( dist ` ndx ) , ( N o. ( -g ` G ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( N o. ( -g ` G ) ) ) >. ) )
34 33 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 ) ) ) >. ) ) )
35 29 34 eqtr4id 
 |-  ( ( G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) )
36 2 str0 
 |-  (/) = ( E ` (/) )
37 fvprc 
 |-  ( -. G e. _V -> ( E ` G ) = (/) )
38 37 adantr 
 |-  ( ( -. G e. _V /\ N e. V ) -> ( E ` G ) = (/) )
39 reldmtng 
 |-  Rel dom toNrmGrp
40 39 ovprc1 
 |-  ( -. G e. _V -> ( G toNrmGrp N ) = (/) )
41 40 adantr 
 |-  ( ( -. G e. _V /\ N e. V ) -> ( G toNrmGrp N ) = (/) )
42 1 41 syl5eq 
 |-  ( ( -. G e. _V /\ N e. V ) -> T = (/) )
43 42 fveq2d 
 |-  ( ( -. G e. _V /\ N e. V ) -> ( E ` T ) = ( E ` (/) ) )
44 36 38 43 3eqtr4a 
 |-  ( ( -. G e. _V /\ N e. V ) -> ( E ` G ) = ( E ` T ) )
45 35 44 pm2.61ian 
 |-  ( N e. V -> ( E ` G ) = ( E ` T ) )