Theorem hhssims

Description: Induced metric of a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsssh2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
	hhssims.2	⊢ 𝐻 ∈ Sℋ
	hhssims.3	⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
Assertion	hhssims	⊢ 𝐷 = ( IndMet ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2		hhssims.2	⊢ 𝐻 ∈ Sℋ
3		hhssims.3	⊢ 𝐷 = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
4	1 2	hhssnv	⊢ 𝑊 ∈ NrmCVec
5	1 2	hhssvs	⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( −𝑣 ‘ 𝑊 )
6	1	hhssnm	⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )
7		eqid	⊢ ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
8	5 6 7	imsval	⊢ ( 𝑊 ∈ NrmCVec → ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) )
9	4 8	ax-mp	⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
10		resco	⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
11	1 2	hhssvsf	⊢ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻
12		frn	⊢ ( ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) : ( 𝐻 × 𝐻 ) ⟶ 𝐻 → ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 )
13	11 12	ax-mp	⊢ ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻
14		cores	⊢ ( ran ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 → ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) )
15	13 14	ax-mp	⊢ ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( normℎ ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
16	10 15	eqtr4i	⊢ ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) ) = ( ( normℎ ↾ 𝐻 ) ∘ ( −ℎ ↾ ( 𝐻 × 𝐻 ) ) )
17	9 16	eqtr4i	⊢ ( IndMet ‘ 𝑊 ) = ( ( normℎ ∘ −ℎ ) ↾ ( 𝐻 × 𝐻 ) )
18	3 17	eqtr4i	⊢ 𝐷 = ( IndMet ‘ 𝑊 )