Metamath Proof Explorer

Theorem isngp3

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

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

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 eqid 
 |-  ( D |` ( X X. X ) ) = ( D |` ( X X. X ) )
6 1 2 3 4 5 isngp2 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) )
7 4 3 msmet2 
 |-  ( G e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )
8 1 4 3 5 nmf2 
 |-  ( ( G e. Grp /\ ( D |` ( X X. X ) ) e. ( Met ` X ) ) -> N : X --> RR )
9 7 8 sylan2 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> N : X --> RR )
10 4 2 grpsubf 
 |-  ( G e. Grp -> .- : ( X X. X ) --> X )
11 10 adantr 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> .- : ( X X. X ) --> X )
12 fco 
 |-  ( ( N : X --> RR /\ .- : ( X X. X ) --> X ) -> ( N o. .- ) : ( X X. X ) --> RR )
13 9 11 12 syl2anc 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( N o. .- ) : ( X X. X ) --> RR )
14 13 ffnd 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( N o. .- ) Fn ( X X. X ) )
15 7 adantl 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( D |` ( X X. X ) ) e. ( Met ` X ) )
16 metf 
 |-  ( ( D |` ( X X. X ) ) e. ( Met ` X ) -> ( D |` ( X X. X ) ) : ( X X. X ) --> RR )
17 ffn 
 |-  ( ( D |` ( X X. X ) ) : ( X X. X ) --> RR -> ( D |` ( X X. X ) ) Fn ( X X. X ) )
18 15 16 17 3syl 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( D |` ( X X. X ) ) Fn ( X X. X ) )
19 eqfnov2 
 |-  ( ( ( N o. .- ) Fn ( X X. X ) /\ ( D |` ( X X. X ) ) Fn ( X X. X ) ) -> ( ( N o. .- ) = ( D |` ( X X. X ) ) <-> A. x e. X A. y e. X ( x ( N o. .- ) y ) = ( x ( D |` ( X X. X ) ) y ) ) )
20 14 18 19 syl2anc 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( ( N o. .- ) = ( D |` ( X X. X ) ) <-> A. x e. X A. y e. X ( x ( N o. .- ) y ) = ( x ( D |` ( X X. X ) ) y ) ) )
21 opelxpi 
 |-  ( ( x e. X /\ y e. X ) -> <. x , y >. e. ( X X. X ) )
22 fvco3 
 |-  ( ( .- : ( X X. X ) --> X /\ <. x , y >. e. ( X X. X ) ) -> ( ( N o. .- ) ` <. x , y >. ) = ( N ` ( .- ` <. x , y >. ) ) )
23 11 21 22 syl2an 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( N o. .- ) ` <. x , y >. ) = ( N ` ( .- ` <. x , y >. ) ) )
24 df-ov 
 |-  ( x ( N o. .- ) y ) = ( ( N o. .- ) ` <. x , y >. )
25 df-ov 
 |-  ( x .- y ) = ( .- ` <. x , y >. )
26 25 fveq2i 
 |-  ( N ` ( x .- y ) ) = ( N ` ( .- ` <. x , y >. ) )
27 23 24 26 3eqtr4g 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( x ( N o. .- ) y ) = ( N ` ( x .- y ) ) )
28 ovres 
 |-  ( ( x e. X /\ y e. X ) -> ( x ( D |` ( X X. X ) ) y ) = ( x D y ) )
29 28 adantl 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( x ( D |` ( X X. X ) ) y ) = ( x D y ) )
30 27 29 eqeq12d 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( N o. .- ) y ) = ( x ( D |` ( X X. X ) ) y ) <-> ( N ` ( x .- y ) ) = ( x D y ) ) )
31 eqcom 
 |-  ( ( N ` ( x .- y ) ) = ( x D y ) <-> ( x D y ) = ( N ` ( x .- y ) ) )
32 30 31 bitrdi 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( N o. .- ) y ) = ( x ( D |` ( X X. X ) ) y ) <-> ( x D y ) = ( N ` ( x .- y ) ) ) )
33 32 2ralbidva 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( A. x e. X A. y e. X ( x ( N o. .- ) y ) = ( x ( D |` ( X X. X ) ) y ) <-> A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
34 20 33 bitrd 
 |-  ( ( G e. Grp /\ G e. MetSp ) -> ( ( N o. .- ) = ( D |` ( X X. X ) ) <-> A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
35 34 pm5.32i 
 |-  ( ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
36 df-3an 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) )
37 df-3an 
 |-  ( ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
38 35 36 37 3bitr4i 
 |-  ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) = ( D |` ( X X. X ) ) ) <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )
39 6 38 bitri 
 |-  ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ A. x e. X A. y e. X ( x D y ) = ( N ` ( x .- y ) ) ) )