Theorem sgrimval

Description: The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008) (Revised by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	sgrim.x	|- X = ( T |`s U )
	sgrim.d	|- D = ( dist ` T )
	sgrim.e	|- E = ( dist ` X )
	sgrimval.t	|- T = ( G toNrmGrp N )
	sgrimval.n	|- N = ( norm ` G )
	sgrimval.s	|- S = ( SubGrp ` T )
Assertion	sgrimval	|- ( ( ( G e. NrmGrp /\ U e. S ) /\ ( A e. U /\ B e. U ) ) -> ( A E B ) = ( A D B ) )

Proof

Step	Hyp	Ref	Expression
1		sgrim.x	|- X = ( T |`s U )
2		sgrim.d	|- D = ( dist ` T )
3		sgrim.e	|- E = ( dist ` X )
4		sgrimval.t	|- T = ( G toNrmGrp N )
5		sgrimval.n	|- N = ( norm ` G )
6		sgrimval.s	|- S = ( SubGrp ` T )
7	1 2 3	sgrim	|- ( U e. S -> E = D )
8	7	oveqd	|- ( U e. S -> ( A E B ) = ( A D B ) )
9	8	ad2antlr	|- ( ( ( G e. NrmGrp /\ U e. S ) /\ ( A e. U /\ B e. U ) ) -> ( A E B ) = ( A D B ) )