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 ) )