Metamath Proof Explorer

Theorem nmpropd

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

Ref Expression
Hypotheses nmpropd.1 
|- ( ph -> ( Base ` K ) = ( Base ` L ) )
nmpropd.2 
|- ( ph -> ( +g ` K ) = ( +g ` L ) )
nmpropd.3 
|- ( ph -> ( dist ` K ) = ( dist ` L ) )
Assertion nmpropd 
|- ( ph -> ( norm ` K ) = ( norm ` L ) )

Proof

Step Hyp Ref Expression
1 nmpropd.1 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
2 nmpropd.2 
 |-  ( ph -> ( +g ` K ) = ( +g ` L ) )
3 nmpropd.3 
 |-  ( ph -> ( dist ` K ) = ( dist ` L ) )
4 eqidd 
 |-  ( ph -> x = x )
5 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
6 2 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
7 5 1 6 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
8 3 4 7 oveq123d 
 |-  ( ph -> ( x ( dist ` K ) ( 0g ` K ) ) = ( x ( dist ` L ) ( 0g ` L ) ) )
9 1 8 mpteq12dv 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( x ( dist ` K ) ( 0g ` K ) ) ) = ( x e. ( Base ` L ) |-> ( x ( dist ` L ) ( 0g ` L ) ) ) )
10 eqid 
 |-  ( norm ` K ) = ( norm ` K )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
13 eqid 
 |-  ( dist ` K ) = ( dist ` K )
14 10 11 12 13 nmfval 
 |-  ( norm ` K ) = ( x e. ( Base ` K ) |-> ( x ( dist ` K ) ( 0g ` K ) ) )
15 eqid 
 |-  ( norm ` L ) = ( norm ` L )
16 eqid 
 |-  ( Base ` L ) = ( Base ` L )
17 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
18 eqid 
 |-  ( dist ` L ) = ( dist ` L )
19 15 16 17 18 nmfval 
 |-  ( norm ` L ) = ( x e. ( Base ` L ) |-> ( x ( dist ` L ) ( 0g ` L ) ) )
20 9 14 19 3eqtr4g 
 |-  ( ph -> ( norm ` K ) = ( norm ` L ) )