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{\upharpoonright }_{𝑠}U$$
	sgrim.d	$$⊢D=\mathrm{dist}\left(T\right)$$
	sgrim.e	$$⊢E=\mathrm{dist}\left(X\right)$$
	sgrimval.t	$$⊢T=G\mathrm{toNrmGrp}N$$
	sgrimval.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	sgrimval.s	$$⊢S=\mathrm{SubGrp}\left(T\right)$$
Assertion	sgrimval	$$⊢\left(\left(G\in \mathrm{NrmGrp}\wedge U\in S\right)\wedge \left(A\in U\wedge B\in U\right)\right)\to AEB=ADB$$

Proof

Step	Hyp	Ref	Expression
1		sgrim.x	$$⊢X=T{\upharpoonright }_{𝑠}U$$
2		sgrim.d	$$⊢D=\mathrm{dist}\left(T\right)$$
3		sgrim.e	$$⊢E=\mathrm{dist}\left(X\right)$$
4		sgrimval.t	$$⊢T=G\mathrm{toNrmGrp}N$$
5		sgrimval.n	$$⊢N=\mathrm{norm}\left(G\right)$$
6		sgrimval.s	$$⊢S=\mathrm{SubGrp}\left(T\right)$$
7	1 2 3	sgrim	$$⊢U\in S\to E=D$$
8	7	oveqd	$$⊢U\in S\to AEB=ADB$$
9	8	ad2antlr	$$⊢\left(\left(G\in \mathrm{NrmGrp}\wedge U\in S\right)\wedge \left(A\in U\wedge B\in U\right)\right)\to AEB=ADB$$