imsdval - Metamath Proof Explorer

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

Theorem imsdval 28243

Description: Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
imsdval.1	⊢ 𝑋 = (BaseSet‘𝑈)
imsdval.3	⊢ 𝑀 = ( −_𝑣 ‘𝑈)
imsdval.6	⊢ 𝑁 = (norm_CV‘𝑈)
imsdval.8	⊢ 𝐷 = (IndMet‘𝑈)

**Assertion**
Ref	Expression
imsdval	⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝑀𝐵)))

**Proof of Theorem imsdval**
Step	Hyp	Ref	Expression
1		imsdval.3	. . . . . 6 ⊢ 𝑀 = ( −_𝑣 ‘𝑈)
2		imsdval.6	. . . . . 6 ⊢ 𝑁 = (norm_CV‘𝑈)
3		imsdval.8	. . . . . 6 ⊢ 𝐷 = (IndMet‘𝑈)
4	1, 2, 3	imsval 28242	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → 𝐷 = (𝑁 ∘ 𝑀))
5	4	3ad2ant1 1113	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐷 = (𝑁 ∘ 𝑀))
6	5	fveq1d 6503	. . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐷‘⟨𝐴, 𝐵⟩) = ((𝑁 ∘ 𝑀)‘⟨𝐴, 𝐵⟩))
7		imsdval.1	. . . . . 6 ⊢ 𝑋 = (BaseSet‘𝑈)
8	7, 1	nvmf 28202	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → 𝑀:(𝑋 × 𝑋)⟶𝑋)
9		opelxpi 5445	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑋))
10		fvco3 6590	. . . . 5 ⊢ ((𝑀:(𝑋 × 𝑋)⟶𝑋 ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑋)) → ((𝑁 ∘ 𝑀)‘⟨𝐴, 𝐵⟩) = (𝑁‘(𝑀‘⟨𝐴, 𝐵⟩)))
11	8, 9, 10	syl2an 586	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑁 ∘ 𝑀)‘⟨𝐴, 𝐵⟩) = (𝑁‘(𝑀‘⟨𝐴, 𝐵⟩)))
12	11	3impb 1095	. . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁 ∘ 𝑀)‘⟨𝐴, 𝐵⟩) = (𝑁‘(𝑀‘⟨𝐴, 𝐵⟩)))
13	6, 12	eqtrd 2814	. 2 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐷‘⟨𝐴, 𝐵⟩) = (𝑁‘(𝑀‘⟨𝐴, 𝐵⟩)))
14		df-ov 6981	. 2 ⊢ (𝐴𝐷𝐵) = (𝐷‘⟨𝐴, 𝐵⟩)
15		df-ov 6981	. . 3 ⊢ (𝐴𝑀𝐵) = (𝑀‘⟨𝐴, 𝐵⟩)
16	15	fveq2i 6504	. 2 ⊢ (𝑁‘(𝐴𝑀𝐵)) = (𝑁‘(𝑀‘⟨𝐴, 𝐵⟩))
17	13, 14, 16	3eqtr4g 2839	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝑀𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ⟨cop 4448 × cxp 5406 ∘ ccom 5412 ⟶wf 6186 ‘cfv 6190 (class class class)co 6978 NrmCVeccnv 28141 BaseSetcba 28143 −_𝑣 cnsb 28146 norm_CVcnmcv 28147 IndMetcims 28148

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-rep 5050 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-reu 3095 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-po 5327 df-so 5328 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-riota 6939 df-ov 6981 df-oprab 6982 df-mpo 6983 df-1st 7503 df-2nd 7504 df-er 8091 df-en 8309 df-dom 8310 df-sdom 8311 df-pnf 10478 df-mnf 10479 df-ltxr 10481 df-sub 10674 df-neg 10675 df-grpo 28050 df-gid 28051 df-ginv 28052 df-gdiv 28053 df-ablo 28102 df-vc 28116 df-nv 28149 df-va 28152 df-ba 28153 df-sm 28154 df-0v 28155 df-vs 28156 df-nmcv 28157 df-ims 28158

This theorem is referenced by: imsdval2 28244 nvnd 28245 vacn 28251 smcnlem 28254 sspimsval 28295 blometi 28360 blocnilem 28361 ubthlem2 28429 minvecolem2 28433 minvecolem4 28438 minvecolem5 28439 minvecolem6 28440 h2hmetdval 28537 hhssmetdval 28837

W3C validator