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 ⊢ 𝐶 = ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ )
cchhllem.1 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
cchhllem.2 ⊢ ( Scalar ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
cchhllem.3 ⊢ ( ·𝑠 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
cchhllem.4 ⊢ ( ·𝑖 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
Assertion cchhllem ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ 𝐶 )

Proof

Step Hyp Ref Expression
1 cchhl.c ⊢ 𝐶 = ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ )
2 cchhllem.1 ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3 cchhllem.2 ⊢ ( Scalar ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
4 cchhllem.3 ⊢ ( ·𝑠 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
5 cchhllem.4 ⊢ ( ·𝑖 ‘ ndx ) ≠ ( 𝐸 ‘ ndx )
6 5 necomi ⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
7 2 6 setsnid ⊢ ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( 𝐸 ‘ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ ) )
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 ⊢ ( ⊤ → ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
14 13 mptru ⊢ ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
15 1 fveq2i ⊢ ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ ) )
16 7 14 15 3eqtr4i ⊢ ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ 𝐶 )