ncvsi - Metamath Proof Explorer

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

Theorem ncvsi 25058

Description: The properties of a normed subcomplex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006.) (Revised by AV, 7-Oct-2021.)

**Hypotheses**
Ref	Expression
isncvsngp.v	⊢ 𝑉 = (Base‘𝑊)
isncvsngp.n	⊢ 𝑁 = (norm‘𝑊)
isncvsngp.s	⊢ · = ( ·_𝑠 ‘𝑊)
isncvsngp.f	⊢ 𝐹 = (Scalar‘𝑊)
isncvsngp.k	⊢ 𝐾 = (Base‘𝐹)
ncvsi.m	⊢ − = (-_g‘𝑊)
ncvsi.0	⊢ 0 = (0_g‘𝑊)

**Assertion**
Ref	Expression
ncvsi	⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) → (𝑊 ∈ ℂVec ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))

Distinct variable groups: 𝑘,𝐹,𝑥 𝑘,𝐾,𝑥 𝑘,𝑁,𝑥 𝑘,𝑉,𝑥 𝑘,𝑊,𝑥 · ,𝑘,𝑥 𝑦,𝑉 𝑦,𝑊,𝑥 Allowed substitution hints: · (𝑦) 𝐹(𝑦) 𝐾(𝑦) − (𝑥,𝑦,𝑘) 𝑁(𝑦) 0 (𝑥,𝑦,𝑘)

**Proof of Theorem ncvsi**
Step	Hyp	Ref	Expression
1		isncvsngp.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
2		isncvsngp.n	. . 3 ⊢ 𝑁 = (norm‘𝑊)
3		isncvsngp.s	. . 3 ⊢ · = ( ·_𝑠 ‘𝑊)
4		isncvsngp.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		isncvsngp.k	. . 3 ⊢ 𝐾 = (Base‘𝐹)
6	1, 2, 3, 4, 5	isncvsngp 25056	. 2 ⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) ↔ (𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
7		simp1 1136	. . 3 ⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → 𝑊 ∈ ℂVec)
8	1, 2	nmf 24509	. . . 4 ⊢ (𝑊 ∈ NrmGrp → 𝑁:𝑉⟶ℝ)
9	8	3ad2ant2 1134	. . 3 ⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → 𝑁:𝑉⟶ℝ)
10		ncvsi.m	. . . . . . 7 ⊢ − = (-_g‘𝑊)
11		ncvsi.0	. . . . . . 7 ⊢ 0 = (0_g‘𝑊)
12	1, 2, 10, 11	ngpi 24522	. . . . . 6 ⊢ (𝑊 ∈ NrmGrp → (𝑊 ∈ Grp ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))))
13		r19.26 3093	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑉 ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) ↔ (∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
14		simpll 766	. . . . . . . . . . 11 ⊢ (((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ))
15		simplr 768	. . . . . . . . . . 11 ⊢ (((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))
16		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))
17	14, 15, 16	3jca 1128	. . . . . . . . . 10 ⊢ (((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
18	17	ralimi 3068	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝑉 ((((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
19	13, 18	sylbir 235	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
20	19	ex 412	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦))) → (∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))
21	20	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑊 ∈ Grp ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)))) → (∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))
22	12, 21	syl 17	. . . . 5 ⊢ (𝑊 ∈ NrmGrp → (∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))
23	22	imp 406	. . . 4 ⊢ ((𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
24	23	3adant1 1130	. . 3 ⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))
25	7, 9, 24	3jca 1128	. 2 ⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) → (𝑊 ∈ ℂVec ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))
26	6, 25	sylbi 217	1 ⊢ (𝑊 ∈ (NrmVec ∩ ℂVec) → (𝑊 ∈ ℂVec ∧ 𝑁:𝑉⟶ℝ ∧ ∀𝑥 ∈ 𝑉 (((𝑁‘𝑥) = 0 ↔ 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 (𝑁‘(𝑥 − 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)) ∧ ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3046 ∩ cin 3921 class class class wbr 5115 ⟶wf 6515 ‘cfv 6519 (class class class)co 7394 ℝcr 11085 0cc0 11086 + caddc 11089 · cmul 11091 ≤ cle 11227 abscabs 15210 Basecbs 17185 Scalarcsca 17229 ·_𝑠 cvsca 17230 0_gc0g 17408 Grpcgrp 18871 -_gcsg 18873 normcnm 24470 NrmGrpcngp 24471 NrmVeccnvc 24475 ℂVecccvs 25029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5242 ax-sep 5259 ax-nul 5269 ax-pow 5328 ax-pr 5395 ax-un 7718 ax-cnex 11142 ax-resscn 11143 ax-1cn 11144 ax-icn 11145 ax-addcl 11146 ax-addrcl 11147 ax-mulcl 11148 ax-mulrcl 11149 ax-mulcom 11150 ax-addass 11151 ax-mulass 11152 ax-distr 11153 ax-i2m1 11154 ax-1ne0 11155 ax-1rid 11156 ax-rnegex 11157 ax-rrecex 11158 ax-cnre 11159 ax-pre-lttri 11160 ax-pre-lttrn 11161 ax-pre-ltadd 11162 ax-pre-mulgt0 11163 ax-pre-sup 11164 ax-addf 11165 ax-mulf 11166

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2880 df-ne 2928 df-nel 3032 df-ral 3047 df-rex 3056 df-rmo 3357 df-reu 3358 df-rab 3412 df-v 3457 df-sbc 3762 df-csb 3871 df-dif 3925 df-un 3927 df-in 3929 df-ss 3939 df-pss 3942 df-nul 4305 df-if 4497 df-pw 4573 df-sn 4598 df-pr 4600 df-tp 4602 df-op 4604 df-uni 4880 df-iun 4965 df-br 5116 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5541 df-eprel 5546 df-po 5554 df-so 5555 df-fr 5599 df-we 5601 df-xp 5652 df-rel 5653 df-cnv 5654 df-co 5655 df-dm 5656 df-rn 5657 df-res 5658 df-ima 5659 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6472 df-fun 6521 df-fn 6522 df-f 6523 df-f1 6524 df-fo 6525 df-f1o 6526 df-fv 6527 df-riota 7351 df-ov 7397 df-oprab 7398 df-mpo 7399 df-om 7851 df-1st 7977 df-2nd 7978 df-frecs 8269 df-wrecs 8300 df-recs 8349 df-rdg 8387 df-1o 8443 df-er 8682 df-map 8805 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-sup 9411 df-inf 9412 df-pnf 11228 df-mnf 11229 df-xr 11230 df-ltxr 11231 df-le 11232 df-sub 11425 df-neg 11426 df-div 11852 df-nn 12198 df-2 12260 df-3 12261 df-4 12262 df-5 12263 df-6 12264 df-7 12265 df-8 12266 df-9 12267 df-n0 12459 df-z 12546 df-dec 12666 df-uz 12810 df-q 12922 df-rp 12966 df-xneg 13085 df-xadd 13086 df-xmul 13087 df-ico 13325 df-fz 13482 df-seq 13977 df-exp 14037 df-cj 15075 df-re 15076 df-im 15077 df-sqrt 15211 df-abs 15212 df-struct 17123 df-sets 17140 df-slot 17158 df-ndx 17170 df-base 17186 df-ress 17207 df-plusg 17239 df-mulr 17240 df-starv 17241 df-tset 17245 df-ple 17246 df-ds 17248 df-unif 17249 df-rest 17391 df-topn 17392 df-0g 17410 df-topgen 17412 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-grp 18874 df-minusg 18875 df-sbg 18876 df-subg 19061 df-cmn 19718 df-abl 19719 df-mgp 20056 df-rng 20068 df-ur 20097 df-ring 20150 df-cring 20151 df-subrng 20461 df-subrg 20485 df-abv 20724 df-psmet 21262 df-xmet 21263 df-met 21264 df-bl 21265 df-mopn 21266 df-cnfld 21271 df-top 22787 df-topon 22804 df-topsp 22826 df-bases 22839 df-xms 24214 df-ms 24215 df-nm 24476 df-ngp 24477 df-nrg 24479 df-nlm 24480 df-nvc 24481 df-clm 24969 df-cvs 25030

This theorem is referenced by: (None)

W3C validator