![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > recvs | Structured version Visualization version GIF version |
Description: The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) |
Ref | Expression |
---|---|
recvs.r | ⊢ 𝑅 = (ringLMod‘ℝfld) |
Ref | Expression |
---|---|
recvs | ⊢ 𝑅 ∈ ℂVec |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | refld 20325 | . . . . . 6 ⊢ ℝfld ∈ Field | |
2 | fldidom 19665 | . . . . . . 7 ⊢ (ℝfld ∈ Field → ℝfld ∈ IDomn) | |
3 | isidom 19664 | . . . . . . . 8 ⊢ (ℝfld ∈ IDomn ↔ (ℝfld ∈ CRing ∧ ℝfld ∈ Domn)) | |
4 | crngring 18911 | . . . . . . . . 9 ⊢ (ℝfld ∈ CRing → ℝfld ∈ Ring) | |
5 | 4 | adantr 474 | . . . . . . . 8 ⊢ ((ℝfld ∈ CRing ∧ ℝfld ∈ Domn) → ℝfld ∈ Ring) |
6 | 3, 5 | sylbi 209 | . . . . . . 7 ⊢ (ℝfld ∈ IDomn → ℝfld ∈ Ring) |
7 | 2, 6 | syl 17 | . . . . . 6 ⊢ (ℝfld ∈ Field → ℝfld ∈ Ring) |
8 | 1, 7 | ax-mp 5 | . . . . 5 ⊢ ℝfld ∈ Ring |
9 | rlmlmod 19565 | . . . . 5 ⊢ (ℝfld ∈ Ring → (ringLMod‘ℝfld) ∈ LMod) | |
10 | 8, 9 | ax-mp 5 | . . . 4 ⊢ (ringLMod‘ℝfld) ∈ LMod |
11 | rlmsca 19560 | . . . . . 6 ⊢ (ℝfld ∈ Field → ℝfld = (Scalar‘(ringLMod‘ℝfld))) | |
12 | 1, 11 | ax-mp 5 | . . . . 5 ⊢ ℝfld = (Scalar‘(ringLMod‘ℝfld)) |
13 | df-refld 20311 | . . . . 5 ⊢ ℝfld = (ℂfld ↾s ℝ) | |
14 | 12, 13 | eqtr3i 2850 | . . . 4 ⊢ (Scalar‘(ringLMod‘ℝfld)) = (ℂfld ↾s ℝ) |
15 | resubdrg 20314 | . . . . 5 ⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing) | |
16 | 15 | simpli 478 | . . . 4 ⊢ ℝ ∈ (SubRing‘ℂfld) |
17 | eqid 2824 | . . . . 5 ⊢ (Scalar‘(ringLMod‘ℝfld)) = (Scalar‘(ringLMod‘ℝfld)) | |
18 | 17 | isclmi 23245 | . . . 4 ⊢ (((ringLMod‘ℝfld) ∈ LMod ∧ (Scalar‘(ringLMod‘ℝfld)) = (ℂfld ↾s ℝ) ∧ ℝ ∈ (SubRing‘ℂfld)) → (ringLMod‘ℝfld) ∈ ℂMod) |
19 | 10, 14, 16, 18 | mp3an 1591 | . . 3 ⊢ (ringLMod‘ℝfld) ∈ ℂMod |
20 | 15 | simpri 481 | . . . 4 ⊢ ℝfld ∈ DivRing |
21 | rlmlvec 19566 | . . . 4 ⊢ (ℝfld ∈ DivRing → (ringLMod‘ℝfld) ∈ LVec) | |
22 | 20, 21 | ax-mp 5 | . . 3 ⊢ (ringLMod‘ℝfld) ∈ LVec |
23 | 19, 22 | elini 4023 | . 2 ⊢ (ringLMod‘ℝfld) ∈ (ℂMod ∩ LVec) |
24 | recvs.r | . 2 ⊢ 𝑅 = (ringLMod‘ℝfld) | |
25 | df-cvs 23292 | . 2 ⊢ ℂVec = (ℂMod ∩ LVec) | |
26 | 23, 24, 25 | 3eltr4i 2918 | 1 ⊢ 𝑅 ∈ ℂVec |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 386 = wceq 1658 ∈ wcel 2166 ∩ cin 3796 ‘cfv 6122 (class class class)co 6904 ℝcr 10250 ↾s cress 16222 Scalarcsca 16307 Ringcrg 18900 CRingccrg 18901 DivRingcdr 19102 Fieldcfield 19103 SubRingcsubrg 19131 LModclmod 19218 LVecclvec 19460 ringLModcrglmod 19529 Domncdomn 19640 IDomncidom 19641 ℂfldccnfld 20105 ℝfldcrefld 20310 ℂModcclm 23230 ℂVecccvs 23291 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-rep 4993 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 ax-cnex 10307 ax-resscn 10308 ax-1cn 10309 ax-icn 10310 ax-addcl 10311 ax-addrcl 10312 ax-mulcl 10313 ax-mulrcl 10314 ax-mulcom 10315 ax-addass 10316 ax-mulass 10317 ax-distr 10318 ax-i2m1 10319 ax-1ne0 10320 ax-1rid 10321 ax-rnegex 10322 ax-rrecex 10323 ax-cnre 10324 ax-pre-lttri 10325 ax-pre-lttrn 10326 ax-pre-ltadd 10327 ax-pre-mulgt0 10328 ax-addf 10330 ax-mulf 10331 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-nel 3102 df-ral 3121 df-rex 3122 df-reu 3123 df-rmo 3124 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-pss 3813 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-tp 4401 df-op 4403 df-uni 4658 df-int 4697 df-iun 4741 df-br 4873 df-opab 4935 df-mpt 4952 df-tr 4975 df-id 5249 df-eprel 5254 df-po 5262 df-so 5263 df-fr 5300 df-we 5302 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-res 5353 df-ima 5354 df-pred 5919 df-ord 5965 df-on 5966 df-lim 5967 df-suc 5968 df-iota 6085 df-fun 6124 df-fn 6125 df-f 6126 df-f1 6127 df-fo 6128 df-f1o 6129 df-fv 6130 df-riota 6865 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-om 7326 df-1st 7427 df-2nd 7428 df-tpos 7616 df-wrecs 7671 df-recs 7733 df-rdg 7771 df-1o 7825 df-oadd 7829 df-er 8008 df-en 8222 df-dom 8223 df-sdom 8224 df-fin 8225 df-pnf 10392 df-mnf 10393 df-xr 10394 df-ltxr 10395 df-le 10396 df-sub 10586 df-neg 10587 df-div 11009 df-nn 11350 df-2 11413 df-3 11414 df-4 11415 df-5 11416 df-6 11417 df-7 11418 df-8 11419 df-9 11420 df-n0 11618 df-z 11704 df-dec 11821 df-uz 11968 df-fz 12619 df-struct 16223 df-ndx 16224 df-slot 16225 df-base 16227 df-sets 16228 df-ress 16229 df-plusg 16317 df-mulr 16318 df-starv 16319 df-sca 16320 df-vsca 16321 df-ip 16322 df-tset 16323 df-ple 16324 df-ds 16326 df-unif 16327 df-0g 16454 df-mgm 17594 df-sgrp 17636 df-mnd 17647 df-grp 17778 df-minusg 17779 df-subg 17941 df-cmn 18547 df-mgp 18843 df-ur 18855 df-ring 18902 df-cring 18903 df-oppr 18976 df-dvdsr 18994 df-unit 18995 df-invr 19025 df-dvr 19036 df-drng 19104 df-field 19105 df-subrg 19133 df-lmod 19220 df-lvec 19461 df-sra 19532 df-rgmod 19533 df-nzr 19618 df-rlreg 19643 df-domn 19644 df-idom 19645 df-cnfld 20106 df-refld 20311 df-clm 23231 df-cvs 23292 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |