Metamath Proof Explorer

Theorem tngngp2

Description: A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngngp2.t 
|- T = ( G toNrmGrp N )
tngngp2.x 
|- X = ( Base ` G )
tngngp2.d 
|- D = ( dist ` T )
Assertion tngngp2 
|- ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ D e. ( Met ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 tngngp2.t 
 |-  T = ( G toNrmGrp N )
2 tngngp2.x 
 |-  X = ( Base ` G )
3 tngngp2.d 
 |-  D = ( dist ` T )
4 ngpgrp 
 |-  ( T e. NrmGrp -> T e. Grp )
5 2 fvexi 
 |-  X e. _V
6 reex 
 |-  RR e. _V
7 fex2 
 |-  ( ( N : X --> RR /\ X e. _V /\ RR e. _V ) -> N e. _V )
8 5 6 7 mp3an23 
 |-  ( N : X --> RR -> N e. _V )
9 2 a1i 
 |-  ( N e. _V -> X = ( Base ` G ) )
10 1 2 tngbas 
 |-  ( N e. _V -> X = ( Base ` T ) )
11 eqid 
 |-  ( +g ` G ) = ( +g ` G )
12 1 11 tngplusg 
 |-  ( N e. _V -> ( +g ` G ) = ( +g ` T ) )
13 12 oveqdr 
 |-  ( ( N e. _V /\ ( x e. X /\ y e. X ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` T ) y ) )
14 9 10 13 grppropd 
 |-  ( N e. _V -> ( G e. Grp <-> T e. Grp ) )
15 8 14 syl 
 |-  ( N : X --> RR -> ( G e. Grp <-> T e. Grp ) )
16 4 15 syl5ibr 
 |-  ( N : X --> RR -> ( T e. NrmGrp -> G e. Grp ) )
17 16 imp 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> G e. Grp )
18 ngpms 
 |-  ( T e. NrmGrp -> T e. MetSp )
19 18 adantl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> T e. MetSp )
20 eqid 
 |-  ( Base ` T ) = ( Base ` T )
21 20 3 msmet2 
 |-  ( T e. MetSp -> ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( Met ` ( Base ` T ) ) )
22 19 21 syl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( Met ` ( Base ` T ) ) )
23 eqid 
 |-  ( -g ` G ) = ( -g ` G )
24 2 23 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( X X. X ) --> X )
25 17 24 syl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( -g ` G ) : ( X X. X ) --> X )
26 fco 
 |-  ( ( N : X --> RR /\ ( -g ` G ) : ( X X. X ) --> X ) -> ( N o. ( -g ` G ) ) : ( X X. X ) --> RR )
27 25 26 syldan 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( N o. ( -g ` G ) ) : ( X X. X ) --> RR )
28 8 adantr 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> N e. _V )
29 1 23 tngds 
 |-  ( N e. _V -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
30 28 29 syl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
31 3 30 eqtr4id 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> D = ( N o. ( -g ` G ) ) )
32 31 feq1d 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( D : ( X X. X ) --> RR <-> ( N o. ( -g ` G ) ) : ( X X. X ) --> RR ) )
33 27 32 mpbird 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> D : ( X X. X ) --> RR )
34 ffn 
 |-  ( D : ( X X. X ) --> RR -> D Fn ( X X. X ) )
35 fnresdm 
 |-  ( D Fn ( X X. X ) -> ( D |` ( X X. X ) ) = D )
36 33 34 35 3syl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( D |` ( X X. X ) ) = D )
37 28 10 syl 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> X = ( Base ` T ) )
38 37 sqxpeqd 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( X X. X ) = ( ( Base ` T ) X. ( Base ` T ) ) )
39 38 reseq2d 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( D |` ( X X. X ) ) = ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) )
40 36 39 eqtr3d 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> D = ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) )
41 37 fveq2d 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( Met ` X ) = ( Met ` ( Base ` T ) ) )
42 22 40 41 3eltr4d 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> D e. ( Met ` X ) )
43 17 42 jca 
 |-  ( ( N : X --> RR /\ T e. NrmGrp ) -> ( G e. Grp /\ D e. ( Met ` X ) ) )
44 15 biimpa 
 |-  ( ( N : X --> RR /\ G e. Grp ) -> T e. Grp )
45 44 adantrr 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> T e. Grp )
46 simprr 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> D e. ( Met ` X ) )
47 8 adantr 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> N e. _V )
48 47 10 syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> X = ( Base ` T ) )
49 48 fveq2d 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( Met ` X ) = ( Met ` ( Base ` T ) ) )
50 46 49 eleqtrd 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> D e. ( Met ` ( Base ` T ) ) )
51 metf 
 |-  ( D e. ( Met ` ( Base ` T ) ) -> D : ( ( Base ` T ) X. ( Base ` T ) ) --> RR )
52 50 51 syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> D : ( ( Base ` T ) X. ( Base ` T ) ) --> RR )
53 ffn 
 |-  ( D : ( ( Base ` T ) X. ( Base ` T ) ) --> RR -> D Fn ( ( Base ` T ) X. ( Base ` T ) ) )
54 fnresdm 
 |-  ( D Fn ( ( Base ` T ) X. ( Base ` T ) ) -> ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) = D )
55 52 53 54 3syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) = D )
56 55 50 eqeltrd 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( Met ` ( Base ` T ) ) )
57 55 fveq2d 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( MetOpen ` ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) = ( MetOpen ` D ) )
58 simprl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> G e. Grp )
59 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
60 1 3 59 tngtopn 
 |-  ( ( G e. Grp /\ N e. _V ) -> ( MetOpen ` D ) = ( TopOpen ` T ) )
61 58 47 60 syl2anc 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( MetOpen ` D ) = ( TopOpen ` T ) )
62 57 61 eqtr2d 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( TopOpen ` T ) = ( MetOpen ` ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) )
63 eqid 
 |-  ( TopOpen ` T ) = ( TopOpen ` T )
64 3 reseq1i 
 |-  ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) = ( ( dist ` T ) |` ( ( Base ` T ) X. ( Base ` T ) ) )
65 63 20 64 isms2 
 |-  ( T e. MetSp <-> ( ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) e. ( Met ` ( Base ` T ) ) /\ ( TopOpen ` T ) = ( MetOpen ` ( D |` ( ( Base ` T ) X. ( Base ` T ) ) ) ) ) )
66 56 62 65 sylanbrc 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> T e. MetSp )
67 simpl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> N : X --> RR )
68 1 2 6 tngnm 
 |-  ( ( G e. Grp /\ N : X --> RR ) -> N = ( norm ` T ) )
69 58 67 68 syl2anc 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> N = ( norm ` T ) )
70 9 10 eqtr3d 
 |-  ( N e. _V -> ( Base ` G ) = ( Base ` T ) )
71 70 12 grpsubpropd 
 |-  ( N e. _V -> ( -g ` G ) = ( -g ` T ) )
72 47 71 syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( -g ` G ) = ( -g ` T ) )
73 69 72 coeq12d 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( N o. ( -g ` G ) ) = ( ( norm ` T ) o. ( -g ` T ) ) )
74 47 29 syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
75 73 74 eqtr3d 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( ( norm ` T ) o. ( -g ` T ) ) = ( dist ` T ) )
76 eqimss 
 |-  ( ( ( norm ` T ) o. ( -g ` T ) ) = ( dist ` T ) -> ( ( norm ` T ) o. ( -g ` T ) ) C_ ( dist ` T ) )
77 75 76 syl 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> ( ( norm ` T ) o. ( -g ` T ) ) C_ ( dist ` T ) )
78 eqid 
 |-  ( norm ` T ) = ( norm ` T )
79 eqid 
 |-  ( -g ` T ) = ( -g ` T )
80 eqid 
 |-  ( dist ` T ) = ( dist ` T )
81 78 79 80 isngp 
 |-  ( T e. NrmGrp <-> ( T e. Grp /\ T e. MetSp /\ ( ( norm ` T ) o. ( -g ` T ) ) C_ ( dist ` T ) ) )
82 45 66 77 81 syl3anbrc 
 |-  ( ( N : X --> RR /\ ( G e. Grp /\ D e. ( Met ` X ) ) ) -> T e. NrmGrp )
83 43 82 impbida 
 |-  ( N : X --> RR -> ( T e. NrmGrp <-> ( G e. Grp /\ D e. ( Met ` X ) ) ) )