nvvop - Metamath Proof Explorer

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

Theorem nvvop 27798

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
nvvop.1	⊢ 𝑊 = (1^st ‘𝑈)
nvvop.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)
nvvop.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)

**Assertion**
Ref	Expression
nvvop	⊢ (𝑈 ∈ NrmCVec → 𝑊 = ⟨𝐺, 𝑆⟩)

**Proof of Theorem nvvop**
Step	Hyp	Ref	Expression
1		vcrel 27749	. . 3 ⊢ Rel CVec_OLD
2		nvss 27782	. . . . 5 ⊢ NrmCVec ⊆ (CVec_OLD × V)
3		nvvop.1	. . . . . . . 8 ⊢ 𝑊 = (1^st ‘𝑈)
4		eqid 2813	. . . . . . . 8 ⊢ (norm_CV‘𝑈) = (norm_CV‘𝑈)
5	3, 4	nvop2 27797	. . . . . . 7 ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨𝑊, (norm_CV‘𝑈)⟩)
6	5	eleq1d 2877	. . . . . 6 ⊢ (𝑈 ∈ NrmCVec → (𝑈 ∈ NrmCVec ↔ ⟨𝑊, (norm_CV‘𝑈)⟩ ∈ NrmCVec))
7	6	ibi 258	. . . . 5 ⊢ (𝑈 ∈ NrmCVec → ⟨𝑊, (norm_CV‘𝑈)⟩ ∈ NrmCVec)
8	2, 7	sseldi 3803	. . . 4 ⊢ (𝑈 ∈ NrmCVec → ⟨𝑊, (norm_CV‘𝑈)⟩ ∈ (CVec_OLD × V))
9		opelxp1 5357	. . . 4 ⊢ (⟨𝑊, (norm_CV‘𝑈)⟩ ∈ (CVec_OLD × V) → 𝑊 ∈ CVec_OLD)
10	8, 9	syl 17	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑊 ∈ CVec_OLD)
11		1st2nd 7449	. . 3 ⊢ ((Rel CVec_OLD ∧ 𝑊 ∈ CVec_OLD) → 𝑊 = ⟨(1^st ‘𝑊), (2^nd ‘𝑊)⟩)
12	1, 10, 11	sylancr 577	. 2 ⊢ (𝑈 ∈ NrmCVec → 𝑊 = ⟨(1^st ‘𝑊), (2^nd ‘𝑊)⟩)
13		nvvop.2	. . . . 5 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
14	13	vafval 27792	. . . 4 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))
15	3	fveq2i 6414	. . . 4 ⊢ (1^st ‘𝑊) = (1^st ‘(1^st ‘𝑈))
16	14, 15	eqtr4i 2838	. . 3 ⊢ 𝐺 = (1^st ‘𝑊)
17		nvvop.4	. . . . 5 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
18	17	smfval 27794	. . . 4 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
19	3	fveq2i 6414	. . . 4 ⊢ (2^nd ‘𝑊) = (2^nd ‘(1^st ‘𝑈))
20	18, 19	eqtr4i 2838	. . 3 ⊢ 𝑆 = (2^nd ‘𝑊)
21	16, 20	opeq12i 4607	. 2 ⊢ ⟨𝐺, 𝑆⟩ = ⟨(1^st ‘𝑊), (2^nd ‘𝑊)⟩
22	12, 21	syl6eqr 2865	1 ⊢ (𝑈 ∈ NrmCVec → 𝑊 = ⟨𝐺, 𝑆⟩)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1637 ∈ wcel 2157 Vcvv 3398 ⟨cop 4383 × cxp 5316 Rel wrel 5323 ‘cfv 6104 1^st c1st 7399 2^nd c2nd 7400 CVec_OLDcvc 27747 NrmCVeccnv 27773 +_𝑣 cpv 27774 ·_𝑠OLD cns 27776 norm_CVcnmcv 27779

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2069 ax-7 2105 ax-8 2159 ax-9 2166 ax-10 2186 ax-11 2202 ax-12 2215 ax-13 2422 ax-ext 2791 ax-sep 4982 ax-nul 4990 ax-pow 5042 ax-pr 5103 ax-un 7182

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2062 df-mo 2635 df-eu 2638 df-clab 2800 df-cleq 2806 df-clel 2809 df-nfc 2944 df-ne 2986 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3400 df-sbc 3641 df-dif 3779 df-un 3781 df-in 3783 df-ss 3790 df-nul 4124 df-if 4287 df-sn 4378 df-pr 4380 df-op 4384 df-uni 4638 df-br 4852 df-opab 4914 df-mpt 4931 df-id 5226 df-xp 5324 df-rel 5325 df-cnv 5326 df-co 5327 df-dm 5328 df-rn 5329 df-res 5330 df-ima 5331 df-iota 6067 df-fun 6106 df-fn 6107 df-f 6108 df-fo 6110 df-fv 6112 df-oprab 6881 df-1st 7401 df-2nd 7402 df-vc 27748 df-nv 27781 df-va 27784 df-sm 27786 df-nmcv 27789

This theorem is referenced by: nvi 27803 nvvc 27804 nvop 27865

W3C validator