Metamath Proof Explorer


Theorem nmpropd2

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

Ref Expression
Hypotheses nmpropd2.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
nmpropd2.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
nmpropd2.3 ( 𝜑𝐾 ∈ Grp )
nmpropd2.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
nmpropd2.5 ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
Assertion nmpropd2 ( 𝜑 → ( norm ‘ 𝐾 ) = ( norm ‘ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 nmpropd2.1 ( 𝜑𝐵 = ( Base ‘ 𝐾 ) )
2 nmpropd2.2 ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
3 nmpropd2.3 ( 𝜑𝐾 ∈ Grp )
4 nmpropd2.4 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
5 nmpropd2.5 ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
6 1 2 eqtr3d ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
7 1 sqxpeqd ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
8 7 reseq2d ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
9 5 8 eqtr3d ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
10 2 sqxpeqd ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
11 10 reseq2d ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
12 9 11 eqtr3d ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
13 eqidd ( 𝜑𝑎 = 𝑎 )
14 1 2 4 grpidpropd ( 𝜑 → ( 0g𝐾 ) = ( 0g𝐿 ) )
15 12 13 14 oveq123d ( 𝜑 → ( 𝑎 ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ( 0g𝐾 ) ) = ( 𝑎 ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ( 0g𝐿 ) ) )
16 6 15 mpteq12dv ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑎 ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ( 0g𝐾 ) ) ) = ( 𝑎 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑎 ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ( 0g𝐿 ) ) ) )
17 eqid ( norm ‘ 𝐾 ) = ( norm ‘ 𝐾 )
18 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19 eqid ( 0g𝐾 ) = ( 0g𝐾 )
20 eqid ( dist ‘ 𝐾 ) = ( dist ‘ 𝐾 )
21 eqid ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
22 17 18 19 20 21 nmfval2 ( 𝐾 ∈ Grp → ( norm ‘ 𝐾 ) = ( 𝑎 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑎 ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ( 0g𝐾 ) ) ) )
23 3 22 syl ( 𝜑 → ( norm ‘ 𝐾 ) = ( 𝑎 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑎 ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ( 0g𝐾 ) ) ) )
24 1 2 4 grppropd ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
25 3 24 mpbid ( 𝜑𝐿 ∈ Grp )
26 eqid ( norm ‘ 𝐿 ) = ( norm ‘ 𝐿 )
27 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
28 eqid ( 0g𝐿 ) = ( 0g𝐿 )
29 eqid ( dist ‘ 𝐿 ) = ( dist ‘ 𝐿 )
30 eqid ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
31 26 27 28 29 30 nmfval2 ( 𝐿 ∈ Grp → ( norm ‘ 𝐿 ) = ( 𝑎 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑎 ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ( 0g𝐿 ) ) ) )
32 25 31 syl ( 𝜑 → ( norm ‘ 𝐿 ) = ( 𝑎 ∈ ( Base ‘ 𝐿 ) ↦ ( 𝑎 ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ( 0g𝐿 ) ) ) )
33 16 23 32 3eqtr4d ( 𝜑 → ( norm ‘ 𝐾 ) = ( norm ‘ 𝐿 ) )