cphsca - Metamath Proof Explorer

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

Theorem cphsca 24248

Description: A subcomplex pre-Hilbert space is a vector space over a subfield of ℂ_fld. (Contributed by Mario Carneiro, 8-Oct-2015.)

**Hypotheses**
Ref	Expression
cphsca.f	⊢ 𝐹 = (Scalar‘𝑊)
cphsca.k	⊢ 𝐾 = (Base‘𝐹)

**Assertion**
Ref	Expression
cphsca	⊢ (𝑊 ∈ ℂPreHil → 𝐹 = (ℂ_fld ↾_s 𝐾))

Proof of Theorem cphsca Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2738	. . . 4 ⊢ (·_𝑖‘𝑊) = (·_𝑖‘𝑊)
3		eqid 2738	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
4		cphsca.f	. . . 4 ⊢ 𝐹 = (Scalar‘𝑊)
5		cphsca.k	. . . 4 ⊢ 𝐾 = (Base‘𝐹)
6	1, 2, 3, 4, 5	iscph 24239	. . 3 ⊢ (𝑊 ∈ ℂPreHil ↔ ((𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂ_fld ↾_s 𝐾)) ∧ (√ “ (𝐾 ∩ (0[,)+∞))) ⊆ 𝐾 ∧ (norm‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (√‘(𝑥(·_𝑖‘𝑊)𝑥)))))
7	6	simp1bi 1143	. 2 ⊢ (𝑊 ∈ ℂPreHil → (𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ 𝐹 = (ℂ_fld ↾_s 𝐾)))
8	7	simp3d 1142	1 ⊢ (𝑊 ∈ ℂPreHil → 𝐹 = (ℂ_fld ↾_s 𝐾))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∩ cin 3882 ⊆ wss 3883 ↦ cmpt 5153 “ cima 5583 ‘cfv 6418 (class class class)co 7255 0cc0 10802 +∞cpnf 10937 [,)cico 13010 √csqrt 14872 Basecbs 16840 ↾_s cress 16867 Scalarcsca 16891 ·_𝑖cip 16893 ℂ_fldccnfld 20510 PreHilcphl 20741 normcnm 23638 NrmModcnlm 23642 ℂPreHilccph 24235

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-nul 5225

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-xp 5586 df-cnv 5588 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fv 6426 df-ov 7258 df-cph 24237

This theorem is referenced by: cphsubrg 24249 cphreccl 24250 cphcjcl 24252 cphqss 24257 cphclm 24258 ipcau 24307 cphsscph 24320 hlprlem 24436 ishl2 24439

W3C validator