Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nmfval Structured version   Visualization version   GIF version

Theorem nmfval 22615
 Description: The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
nmfval.n 𝑁 = (norm‘𝑊)
nmfval.x 𝑋 = (Base‘𝑊)
nmfval.z 0 = (0g𝑊)
nmfval.d 𝐷 = (dist‘𝑊)
Assertion
Ref Expression
nmfval 𝑁 = (𝑥𝑋 ↦ (𝑥𝐷 0 ))
Distinct variable groups:   𝑥,𝐷   𝑥,𝑊   𝑥,𝑋   𝑥, 0
Allowed substitution hint:   𝑁(𝑥)

Proof of Theorem nmfval
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 nmfval.n . 2 𝑁 = (norm‘𝑊)
2 fveq2 6354 . . . . . 6 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
3 nmfval.x . . . . . 6 𝑋 = (Base‘𝑊)
42, 3syl6eqr 2813 . . . . 5 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑋)
5 fveq2 6354 . . . . . . 7 (𝑤 = 𝑊 → (dist‘𝑤) = (dist‘𝑊))
6 nmfval.d . . . . . . 7 𝐷 = (dist‘𝑊)
75, 6syl6eqr 2813 . . . . . 6 (𝑤 = 𝑊 → (dist‘𝑤) = 𝐷)
8 eqidd 2762 . . . . . 6 (𝑤 = 𝑊𝑥 = 𝑥)
9 fveq2 6354 . . . . . . 7 (𝑤 = 𝑊 → (0g𝑤) = (0g𝑊))
10 nmfval.z . . . . . . 7 0 = (0g𝑊)
119, 10syl6eqr 2813 . . . . . 6 (𝑤 = 𝑊 → (0g𝑤) = 0 )
127, 8, 11oveq123d 6836 . . . . 5 (𝑤 = 𝑊 → (𝑥(dist‘𝑤)(0g𝑤)) = (𝑥𝐷 0 ))
134, 12mpteq12dv 4886 . . . 4 (𝑤 = 𝑊 → (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤))) = (𝑥𝑋 ↦ (𝑥𝐷 0 )))
14 df-nm 22609 . . . 4 norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g𝑤))))
15 eqid 2761 . . . . . 6 (𝑥𝑋 ↦ (𝑥𝐷 0 )) = (𝑥𝑋 ↦ (𝑥𝐷 0 ))
16 df-ov 6818 . . . . . . . 8 (𝑥𝐷 0 ) = (𝐷‘⟨𝑥, 0 ⟩)
17 fvrn0 6379 . . . . . . . 8 (𝐷‘⟨𝑥, 0 ⟩) ∈ (ran 𝐷 ∪ {∅})
1816, 17eqeltri 2836 . . . . . . 7 (𝑥𝐷 0 ) ∈ (ran 𝐷 ∪ {∅})
1918a1i 11 . . . . . 6 (𝑥𝑋 → (𝑥𝐷 0 ) ∈ (ran 𝐷 ∪ {∅}))
2015, 19fmpti 6548 . . . . 5 (𝑥𝑋 ↦ (𝑥𝐷 0 )):𝑋⟶(ran 𝐷 ∪ {∅})
21 fvex 6364 . . . . . 6 (Base‘𝑊) ∈ V
223, 21eqeltri 2836 . . . . 5 𝑋 ∈ V
23 fvex 6364 . . . . . . . 8 (dist‘𝑊) ∈ V
246, 23eqeltri 2836 . . . . . . 7 𝐷 ∈ V
2524rnex 7267 . . . . . 6 ran 𝐷 ∈ V
26 p0ex 5003 . . . . . 6 {∅} ∈ V
2725, 26unex 7123 . . . . 5 (ran 𝐷 ∪ {∅}) ∈ V
28 fex2 7288 . . . . 5 (((𝑥𝑋 ↦ (𝑥𝐷 0 )):𝑋⟶(ran 𝐷 ∪ {∅}) ∧ 𝑋 ∈ V ∧ (ran 𝐷 ∪ {∅}) ∈ V) → (𝑥𝑋 ↦ (𝑥𝐷 0 )) ∈ V)
2920, 22, 27, 28mp3an 1573 . . . 4 (𝑥𝑋 ↦ (𝑥𝐷 0 )) ∈ V
3013, 14, 29fvmpt 6446 . . 3 (𝑊 ∈ V → (norm‘𝑊) = (𝑥𝑋 ↦ (𝑥𝐷 0 )))
31 fvprc 6348 . . . . 5 𝑊 ∈ V → (norm‘𝑊) = ∅)
32 mpt0 6183 . . . . 5 (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 )) = ∅
3331, 32syl6eqr 2813 . . . 4 𝑊 ∈ V → (norm‘𝑊) = (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 )))
34 fvprc 6348 . . . . . 6 𝑊 ∈ V → (Base‘𝑊) = ∅)
353, 34syl5eq 2807 . . . . 5 𝑊 ∈ V → 𝑋 = ∅)
3635mpteq1d 4891 . . . 4 𝑊 ∈ V → (𝑥𝑋 ↦ (𝑥𝐷 0 )) = (𝑥 ∈ ∅ ↦ (𝑥𝐷 0 )))
3733, 36eqtr4d 2798 . . 3 𝑊 ∈ V → (norm‘𝑊) = (𝑥𝑋 ↦ (𝑥𝐷 0 )))
3830, 37pm2.61i 176 . 2 (norm‘𝑊) = (𝑥𝑋 ↦ (𝑥𝐷 0 ))
391, 38eqtri 2783 1 𝑁 = (𝑥𝑋 ↦ (𝑥𝐷 0 ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1632   ∈ wcel 2140  Vcvv 3341   ∪ cun 3714  ∅c0 4059  {csn 4322  ⟨cop 4328   ↦ cmpt 4882  ran crn 5268  ⟶wf 6046  ‘cfv 6050  (class class class)co 6815  Basecbs 16080  distcds 16173  0gc0g 16323  normcnm 22603 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-fv 6058  df-ov 6818  df-nm 22609 This theorem is referenced by:  nmval  22616  nmfval2  22617  nmpropd  22620  subgnm  22659  tngnm  22677  cnfldnm  22804  nmcn  22869  ressnm  29982
 Copyright terms: Public domain W3C validator