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