Metamath Proof Explorer

Theorem cchhllem

Description: Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019) (Revised by AV, 29-Oct-2024)

Ref Expression
Hypotheses cchhl.c ⊢ C = subringAlg ⁡ ℂ fld ⁡ ℝ sSet ⋅ 𝑖 ⁡ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ‾
cchhllem.1 ⊢ E = Slot E ⁡ ndx
cchhllem.2 ⊢ Scalar ⁡ ndx ≠ E ⁡ ndx
cchhllem.3 ⊢ ⋅ ndx ≠ E ⁡ ndx
cchhllem.4 ⊢ ⋅ 𝑖 ⁡ ndx ≠ E ⁡ ndx
Assertion cchhllem ⊢ E ⁡ ℂ fld = E ⁡ C

Proof

Step Hyp Ref Expression
1 cchhl.c ⊢ C = subringAlg ⁡ ℂ fld ⁡ ℝ sSet ⋅ 𝑖 ⁡ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ‾
2 cchhllem.1 ⊢ E = Slot E ⁡ ndx
3 cchhllem.2 ⊢ Scalar ⁡ ndx ≠ E ⁡ ndx
4 cchhllem.3 ⊢ ⋅ ndx ≠ E ⁡ ndx
5 cchhllem.4 ⊢ ⋅ 𝑖 ⁡ ndx ≠ E ⁡ ndx
6 5 necomi ⊢ E ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
7 2 6 setsnid ⊢ E ⁡ subringAlg ⁡ ℂ fld ⁡ ℝ = E ⁡ subringAlg ⁡ ℂ fld ⁡ ℝ sSet ⋅ 𝑖 ⁡ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ‾
8 eqidd ⊢ ⊤ → subringAlg ⁡ ℂ fld ⁡ ℝ = subringAlg ⁡ ℂ fld ⁡ ℝ
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 cnfldbas ⊢ ℂ = Base ℂ fld
11 9 10 sseqtri ⊢ ℝ ⊆ Base ℂ fld
12 11 a1i ⊢ ⊤ → ℝ ⊆ Base ℂ fld
13 8 12 2 3 4 5 sralem ⊢ ⊤ → E ⁡ ℂ fld = E ⁡ subringAlg ⁡ ℂ fld ⁡ ℝ
14 13 mptru ⊢ E ⁡ ℂ fld = E ⁡ subringAlg ⁡ ℂ fld ⁡ ℝ
15 1 fveq2i ⊢ E ⁡ C = E ⁡ subringAlg ⁡ ℂ fld ⁡ ℝ sSet ⋅ 𝑖 ⁡ ndx x ∈ ℂ , y ∈ ℂ ⟼ x ⁢ y ‾
16 7 14 15 3eqtr4i ⊢ E ⁡ ℂ fld = E ⁡ C