Theorem isngp

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 )
Assertion	isngp	|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )

Proof

Step	Hyp	Ref	Expression
1		isngp.n	|- N = ( norm ` G )
2		isngp.z	|- .- = ( -g ` G )
3		isngp.d	|- D = ( dist ` G )
4		elin	|- ( G e. ( Grp i^i MetSp ) <-> ( G e. Grp /\ G e. MetSp ) )
5	4	anbi1i	|- ( ( G e. ( Grp i^i MetSp ) /\ ( N o. .- ) C_ D ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
6		fveq2	|- ( g = G -> ( norm ` g ) = ( norm ` G ) )
7	6 1	eqtr4di	|- ( g = G -> ( norm ` g ) = N )
8		fveq2	|- ( g = G -> ( -g ` g ) = ( -g ` G ) )
9	8 2	eqtr4di	|- ( g = G -> ( -g ` g ) = .- )
10	7 9	coeq12d	|- ( g = G -> ( ( norm ` g ) o. ( -g ` g ) ) = ( N o. .- ) )
11		fveq2	|- ( g = G -> ( dist ` g ) = ( dist ` G ) )
12	11 3	eqtr4di	|- ( g = G -> ( dist ` g ) = D )
13	10 12	sseq12d	|- ( g = G -> ( ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) <-> ( N o. .- ) C_ D ) )
14		df-ngp	|- NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
15	13 14	elrab2	|- ( G e. NrmGrp <-> ( G e. ( Grp i^i MetSp ) /\ ( N o. .- ) C_ D ) )
16		df-3an	|- ( ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) <-> ( ( G e. Grp /\ G e. MetSp ) /\ ( N o. .- ) C_ D ) )
17	5 15 16	3bitr4i	|- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )