Theorem nmpropd

Description: Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmpropd.1	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
	nmpropd.2	⊢ ( 𝜑 → ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 ) )
	nmpropd.3	⊢ ( 𝜑 → ( dist ‘ 𝐾 ) = ( dist ‘ 𝐿 ) )
Assertion	nmpropd	⊢ ( 𝜑 → ( norm ‘ 𝐾 ) = ( norm ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		nmpropd.1	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
2		nmpropd.2	⊢ ( 𝜑 → ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 ) )
3		nmpropd.3	⊢ ( 𝜑 → ( dist ‘ 𝐾 ) = ( dist ‘ 𝐿 ) )
4		eqidd	⊢ ( 𝜑 → 𝑥 = 𝑥 )
5		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
6	2	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
7	5 1 6	grpidpropd	⊢ ( 𝜑 → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐿 ) )
8	3 4 7	oveq123d	⊢ ( 𝜑 → ( 𝑥 ( dist ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) = ( 𝑥 ( dist ‘ 𝐿 ) ( 0g ‘ 𝐿 ) ) )
9	1 8	mpteq12dv	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑥 ( dist ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑥 ( dist ‘ 𝐿 ) ( 0g ‘ 𝐿 ) ) ) )
10		eqid	⊢ ( norm ‘ 𝐾 ) = ( norm ‘ 𝐾 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
13		eqid	⊢ ( dist ‘ 𝐾 ) = ( dist ‘ 𝐾 )
14	10 11 12 13	nmfval	⊢ ( norm ‘ 𝐾 ) = ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑥 ( dist ‘ 𝐾 ) ( 0g ‘ 𝐾 ) ) )
15		eqid	⊢ ( norm ‘ 𝐿 ) = ( norm ‘ 𝐿 )
16		eqid	⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
17		eqid	⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
18		eqid	⊢ ( dist ‘ 𝐿 ) = ( dist ‘ 𝐿 )
19	15 16 17 18	nmfval	⊢ ( norm ‘ 𝐿 ) = ( 𝑥 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑥 ( dist ‘ 𝐿 ) ( 0g ‘ 𝐿 ) ) )
20	9 14 19	3eqtr4g	⊢ ( 𝜑 → ( norm ‘ 𝐾 ) = ( norm ‘ 𝐿 ) )