Metamath Proof Explorer

Theorem isngp2

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses isngp.n 
|- N = ( norm ` G )
isngp.z 
|- .- = ( -g ` G )
isngp.d 
|- D = ( dist ` G )
isngp2.x 
|- X = ( Base ` G )
isngp2.e 
|- E = ( D |` ( X X. X ) )
Assertion isngp2 
|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) )

Proof

Step Hyp Ref Expression
1 isngp.n 
 |-  N = ( norm ` G )
2 isngp.z 
 |-  .- = ( -g ` G )
3 isngp.d 
 |-  D = ( dist ` G )
4 isngp2.x 
 |-  X = ( Base ` G )
5 isngp2.e 
 |-  E = ( D |` ( X X. X ) )
6 1 2 3 isngp 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )
7 resss 
 |-  ( D |` ( X X. X ) ) C_ D
8 5 7 eqsstri 
 |-  E C_ D
9 sseq1 
 |-  ( ( N o. .- ) = E -> ( ( N o. .- ) C_ D <-> E C_ D ) )
10 8 9 mpbiri 
 |-  ( ( N o. .- ) = E -> ( N o. .- ) C_ D )
11 3 reseq1i 
 |-  ( D |` ( X X. X ) ) = ( ( dist ` G ) |` ( X X. X ) )
12 5 11 eqtri 
 |-  E = ( ( dist ` G ) |` ( X X. X ) )
13 4 12 msmet 
 |-  ( G e. MetSp -> E e. ( Met ` X ) )
14 1 4 3 5 nmf2 
 |-  ( ( G e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )
15 13 14 sylan2 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> N : X --> RR )
16 4 2 grpsubf 
 |-  ( G e. Grp -> .- : ( X X. X ) --> X )
17 16 ad2antrr 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> .- : ( X X. X ) --> X )
18 fco 
 |-  ( ( N : X --> RR /\ .- : ( X X. X ) --> X ) -> ( N o. .- ) : ( X X. X ) --> RR )
19 15 17 18 syl2an2r 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) : ( X X. X ) --> RR )
20 19 fdmd 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> dom ( N o. .- ) = ( X X. X ) )
21 20 reseq2d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( E |` dom ( N o. .- ) ) = ( E |` ( X X. X ) ) )
22 4 12 msf 
 |-  ( G e. MetSp -> E : ( X X. X ) --> RR )
23 22 ad2antlr 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> E : ( X X. X ) --> RR )
24 23 ffund 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> Fun E )
25 simpr 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) C_ D )
26 ssv 
 |-  RR C_ _V
27 fss 
 |-  ( ( ( N o. .- ) : ( X X. X ) --> RR /\ RR C_ _V ) -> ( N o. .- ) : ( X X. X ) --> _V )
28 19 26 27 sylancl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) : ( X X. X ) --> _V )
29 fssxp 
 |-  ( ( N o. .- ) : ( X X. X ) --> _V -> ( N o. .- ) C_ ( ( X X. X ) X. _V ) )
30 28 29 syl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) C_ ( ( X X. X ) X. _V ) )
31 25 30 ssind 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) C_ ( D i^i ( ( X X. X ) X. _V ) ) )
32 df-res 
 |-  ( D |` ( X X. X ) ) = ( D i^i ( ( X X. X ) X. _V ) )
33 5 32 eqtri 
 |-  E = ( D i^i ( ( X X. X ) X. _V ) )
34 31 33 sseqtrrdi 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) C_ E )
35 funssres 
 |-  ( ( Fun E /\ ( N o. .- ) C_ E ) -> ( E |` dom ( N o. .- ) ) = ( N o. .- ) )
36 24 34 35 syl2anc 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( E |` dom ( N o. .- ) ) = ( N o. .- ) )
37 ffn 
 |-  ( E : ( X X. X ) --> RR -> E Fn ( X X. X ) )
38 fnresdm 
 |-  ( E Fn ( X X. X ) -> ( E |` ( X X. X ) ) = E )
39 23 37 38 3syl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( E |` ( X X. X ) ) = E )
40 21 36 39 3eqtr3d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) -> ( N o. .- ) = E )
41 40 ex 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( ( N o. .- ) C_ D -> ( N o. .- ) = E ) )
42 10 41 impbid2 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( ( N o. .- ) = E <-> ( N o. .- ) C_ D ) )
43 42 pm5.32i 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) = E ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
44 df-3an 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) = E ) )
45 df-3an 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
46 43 44 45 3bitr4i 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )
47 6 46 bitr4i 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = E ) )