Metamath Proof Explorer

Theorem ccfldsrarelvec

Description: The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023)

Ref Expression
Assertion ccfldsrarelvec ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec

Proof

Step Hyp Ref Expression
1 cnring ⊢ ℂfld ∈ Ring
2 ax-resscn ⊢ ℝ ⊆ ℂ
3 eqidd ⊢ ( ⊤ → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
4 3 mptru ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℂfld ) ‘ ℝ )
5 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
6 4 5 sraring ⊢ ( ( ℂfld ∈ Ring ∧ ℝ ⊆ ℂ ) → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Ring )
7 1 2 6 mp2an ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Ring
8 ringgrp ⊢ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Ring → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Grp )
9 7 8 ax-mp ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Grp
10 refld ⊢ ℝfld ∈ Field
11 isfld ⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
12 10 11 mpbi ⊢ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing )
13 12 simpli ⊢ ℝfld ∈ DivRing
14 drngring ⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring )
15 13 14 ax-mp ⊢ ℝfld ∈ Ring
16 simpr1 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑏 ∈ ℝ )
17 16 recnd ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑏 ∈ ℂ )
18 simpr3 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑦 ∈ ℂ )
19 17 18 mulcld ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑏 · 𝑦 ) ∈ ℂ )
20 simpr2 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑥 ∈ ℂ )
21 17 18 20 adddid ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) )
22 simpl ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑎 ∈ ℝ )
23 22 recnd ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑎 ∈ ℂ )
24 23 17 18 adddird ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) )
25 19 21 24 3jca ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑏 · 𝑦 ) ∈ ℂ ∧ ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) )
26 23 17 18 mulassd ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑎 · 𝑏 ) · 𝑦 ) = ( 𝑎 · ( 𝑏 · 𝑦 ) ) )
27 18 mulid2d ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 1 · 𝑦 ) = 𝑦 )
28 25 26 27 jca32 ⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( ( 𝑏 · 𝑦 ) ∈ ℂ ∧ ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) ∧ ( ( ( 𝑎 · 𝑏 ) · 𝑦 ) = ( 𝑎 · ( 𝑏 · 𝑦 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) ) )
29 28 ralrimivvva ⊢ ( 𝑎 ∈ ℝ → ∀ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( 𝑏 · 𝑦 ) ∈ ℂ ∧ ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) ∧ ( ( ( 𝑎 · 𝑏 ) · 𝑦 ) = ( 𝑎 · ( 𝑏 · 𝑦 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) ) )
30 29 rgen ⊢ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( 𝑏 · 𝑦 ) ∈ ℂ ∧ ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) ∧ ( ( ( 𝑎 · 𝑏 ) · 𝑦 ) = ( 𝑎 · ( 𝑏 · 𝑦 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) )
31 2 5 sseqtri ⊢ ℝ ⊆ ( Base ‘ ℂfld )
32 31 a1i ⊢ ( ⊤ → ℝ ⊆ ( Base ‘ ℂfld ) )
33 3 32 srabase ⊢ ( ⊤ → ( Base ‘ ℂfld ) = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
34 33 mptru ⊢ ( Base ‘ ℂfld ) = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
35 5 34 eqtri ⊢ ℂ = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
36 cnfldadd ⊢ + = ( +g ‘ ℂfld )
37 3 32 sraaddg ⊢ ( ⊤ → ( +g ‘ ℂfld ) = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
38 37 mptru ⊢ ( +g ‘ ℂfld ) = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
39 36 38 eqtri ⊢ + = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
40 cnfldmul ⊢ · = ( .r ‘ ℂfld )
41 3 32 sravsca ⊢ ( ⊤ → ( .r ‘ ℂfld ) = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
42 41 mptru ⊢ ( .r ‘ ℂfld ) = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
43 40 42 eqtri ⊢ · = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
44 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
45 3 32 srasca ⊢ ( ⊤ → ( ℂfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
46 45 mptru ⊢ ( ℂfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
47 44 46 eqtri ⊢ ℝfld = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
48 rebase ⊢ ℝ = ( Base ‘ ℝfld )
49 replusg ⊢ + = ( +g ‘ ℝfld )
50 remulr ⊢ · = ( .r ‘ ℝfld )
51 re1r ⊢ 1 = ( 1r ‘ ℝfld )
52 35 39 43 47 48 49 50 51 islmod ⊢ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod ↔ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ Grp ∧ ℝfld ∈ Ring ∧ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( 𝑏 · 𝑦 ) ∈ ℂ ∧ ( 𝑏 · ( 𝑦 + 𝑥 ) ) = ( ( 𝑏 · 𝑦 ) + ( 𝑏 · 𝑥 ) ) ∧ ( ( 𝑎 + 𝑏 ) · 𝑦 ) = ( ( 𝑎 · 𝑦 ) + ( 𝑏 · 𝑦 ) ) ) ∧ ( ( ( 𝑎 · 𝑏 ) · 𝑦 ) = ( 𝑎 · ( 𝑏 · 𝑦 ) ) ∧ ( 1 · 𝑦 ) = 𝑦 ) ) ) )
53 9 15 30 52 mpbir3an ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod
54 47 islvec ⊢ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec ↔ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod ∧ ℝfld ∈ DivRing ) )
55 53 13 54 mpbir2an ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec