Metamath Proof Explorer

Theorem nmpropd2

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

Ref Expression
Hypotheses nmpropd2.1 
|- ( ph -> B = ( Base ` K ) )
nmpropd2.2 
|- ( ph -> B = ( Base ` L ) )
nmpropd2.3 
|- ( ph -> K e. Grp )
nmpropd2.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
nmpropd2.5 
|- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
Assertion nmpropd2 
|- ( ph -> ( norm ` K ) = ( norm ` L ) )

Proof

Step Hyp Ref Expression
1 nmpropd2.1 
 |-  ( ph -> B = ( Base ` K ) )
2 nmpropd2.2 
 |-  ( ph -> B = ( Base ` L ) )
3 nmpropd2.3 
 |-  ( ph -> K e. Grp )
4 nmpropd2.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
5 nmpropd2.5 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )
6 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
7 1 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` K ) X. ( Base ` K ) ) )
8 7 reseq2d 
 |-  ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
9 5 8 eqtr3d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
10 2 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( ( Base ` L ) X. ( Base ` L ) ) )
11 10 reseq2d 
 |-  ( ph -> ( ( dist ` L ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
12 9 11 eqtr3d 
 |-  ( ph -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) )
13 eqidd 
 |-  ( ph -> a = a )
14 1 2 4 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
15 12 13 14 oveq123d 
 |-  ( ph -> ( a ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ( 0g ` K ) ) = ( a ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ( 0g ` L ) ) )
16 6 15 mpteq12dv 
 |-  ( ph -> ( a e. ( Base ` K ) |-> ( a ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ( 0g ` K ) ) ) = ( a e. ( Base ` L ) |-> ( a ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ( 0g ` L ) ) ) )
17 eqid 
 |-  ( norm ` K ) = ( norm ` K )
18 eqid 
 |-  ( Base ` K ) = ( Base ` K )
19 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
20 eqid 
 |-  ( dist ` K ) = ( dist ` K )
21 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
22 17 18 19 20 21 nmfval2 
 |-  ( K e. Grp -> ( norm ` K ) = ( a e. ( Base ` K ) |-> ( a ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ( 0g ` K ) ) ) )
23 3 22 syl 
 |-  ( ph -> ( norm ` K ) = ( a e. ( Base ` K ) |-> ( a ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) ( 0g ` K ) ) ) )
24 1 2 4 grppropd 
 |-  ( ph -> ( K e. Grp <-> L e. Grp ) )
25 3 24 mpbid 
 |-  ( ph -> L e. Grp )
26 eqid 
 |-  ( norm ` L ) = ( norm ` L )
27 eqid 
 |-  ( Base ` L ) = ( Base ` L )
28 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
29 eqid 
 |-  ( dist ` L ) = ( dist ` L )
30 eqid 
 |-  ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) = ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) )
31 26 27 28 29 30 nmfval2 
 |-  ( L e. Grp -> ( norm ` L ) = ( a e. ( Base ` L ) |-> ( a ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ( 0g ` L ) ) ) )
32 25 31 syl 
 |-  ( ph -> ( norm ` L ) = ( a e. ( Base ` L ) |-> ( a ( ( dist ` L ) |` ( ( Base ` L ) X. ( Base ` L ) ) ) ( 0g ` L ) ) ) )
33 16 23 32 3eqtr4d 
 |-  ( ph -> ( norm ` K ) = ( norm ` L ) )