Metamath Proof Explorer

Theorem nmfval

Description: The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
nmfval.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
nmfval.z ⊢ 0 = ( 0g ‘ 𝑊 )
nmfval.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
Assertion nmfval 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) )

Proof

Step Hyp Ref Expression
1 nmfval.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
2 nmfval.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
3 nmfval.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 nmfval.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
5 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
6 5 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑋 )
7 fveq2 ⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑤 ) = ( dist ‘ 𝑊 ) )
8 7 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( dist ‘ 𝑤 ) = 𝐷 )
9 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝑊 ) )
11 10 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ 𝑤 ) = 0 )
12 8 9 11 oveq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) = ( 𝑥 𝐷 0 ) )
13 6 12 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) )
14 df-nm ⊢ norm = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( 𝑥 ( dist ‘ 𝑤 ) ( 0g ‘ 𝑤 ) ) ) )
15 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) )
16 df-ov ⊢ ( 𝑥 𝐷 0 ) = ( 𝐷 ‘ ⟨ 𝑥 , 0 ⟩ )
17 fvrn0 ⊢ ( 𝐷 ‘ ⟨ 𝑥 , 0 ⟩ ) ∈ ( ran 𝐷 ∪ { ∅ } )
18 16 17 eqeltri ⊢ ( 𝑥 𝐷 0 ) ∈ ( ran 𝐷 ∪ { ∅ } )
19 18 a1i ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑥 𝐷 0 ) ∈ ( ran 𝐷 ∪ { ∅ } ) )
20 15 19 fmpti ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) : 𝑋 ⟶ ( ran 𝐷 ∪ { ∅ } )
21 2 fvexi ⊢ 𝑋 ∈ V
22 4 fvexi ⊢ 𝐷 ∈ V
23 22 rnex ⊢ ran 𝐷 ∈ V
24 p0ex ⊢ { ∅ } ∈ V
25 23 24 unex ⊢ ( ran 𝐷 ∪ { ∅ } ) ∈ V
26 fex2 ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) : 𝑋 ⟶ ( ran 𝐷 ∪ { ∅ } ) ∧ 𝑋 ∈ V ∧ ( ran 𝐷 ∪ { ∅ } ) ∈ V ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) ∈ V )
27 20 21 25 26 mp3an ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) ∈ V
28 13 14 27 fvmpt ⊢ ( 𝑊 ∈ V → ( norm ‘ 𝑊 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) )
29 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( norm ‘ 𝑊 ) = ∅ )
30 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( 𝑥 𝐷 0 ) ) = ∅
31 29 30 eqtr4di ⊢ ( ¬ 𝑊 ∈ V → ( norm ‘ 𝑊 ) = ( 𝑥 ∈ ∅ ↦ ( 𝑥 𝐷 0 ) ) )
32 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
33 2 32 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝑋 = ∅ )
34 33 mpteq1d ⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑥 𝐷 0 ) ) )
35 31 34 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( norm ‘ 𝑊 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) ) )
36 28 35 pm2.61i ⊢ ( norm ‘ 𝑊 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) )
37 1 36 eqtri ⊢ 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐷 0 ) )