# Metamath Proof Explorer

## Theorem cchhllem

Description: Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019)

Ref Expression
Hypotheses cchhl.c ${⊢}{C}=\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({x}\in ℂ,{y}\in ℂ⟼{x}\stackrel{‾}{{y}}\right)⟩$
cchhllem.2 ${⊢}{E}=\mathrm{Slot}{N}$
cchhllem.3 ${⊢}{N}\in ℕ$
cchhllem.4 ${⊢}\left({N}<5\vee 8<{N}\right)$
Assertion cchhllem ${⊢}{E}\left({ℂ}_{\mathrm{fld}}\right)={E}\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 cchhl.c ${⊢}{C}=\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({x}\in ℂ,{y}\in ℂ⟼{x}\stackrel{‾}{{y}}\right)⟩$
2 cchhllem.2 ${⊢}{E}=\mathrm{Slot}{N}$
3 cchhllem.3 ${⊢}{N}\in ℕ$
4 cchhllem.4 ${⊢}\left({N}<5\vee 8<{N}\right)$
5 2 3 ndxid ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
6 5lt8 ${⊢}5<8$
7 3 nnrei ${⊢}{N}\in ℝ$
8 5re ${⊢}5\in ℝ$
9 8re ${⊢}8\in ℝ$
10 7 8 9 lttri ${⊢}\left({N}<5\wedge 5<8\right)\to {N}<8$
11 6 10 mpan2 ${⊢}{N}<5\to {N}<8$
12 7 9 ltnei ${⊢}{N}<8\to 8\ne {N}$
13 11 12 syl ${⊢}{N}<5\to 8\ne {N}$
14 13 necomd ${⊢}{N}<5\to {N}\ne 8$
15 9 7 ltnei ${⊢}8<{N}\to {N}\ne 8$
16 14 15 jaoi ${⊢}\left({N}<5\vee 8<{N}\right)\to {N}\ne 8$
17 4 16 ax-mp ${⊢}{N}\ne 8$
18 2 3 ndxarg ${⊢}{E}\left(\mathrm{ndx}\right)={N}$
19 ipndx ${⊢}{\cdot }_{𝑖}\left(\mathrm{ndx}\right)=8$
20 18 19 neeq12i ${⊢}{E}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)↔{N}\ne 8$
21 17 20 mpbir ${⊢}{E}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$
22 5 21 setsnid ${⊢}{E}\left(\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)={E}\left(\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({x}\in ℂ,{y}\in ℂ⟼{x}\stackrel{‾}{{y}}\right)⟩\right)$
23 eqidd ${⊢}\top \to \mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)=\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)$
24 ax-resscn ${⊢}ℝ\subseteq ℂ$
25 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
26 24 25 sseqtri ${⊢}ℝ\subseteq {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
27 26 a1i ${⊢}\top \to ℝ\subseteq {\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
28 23 27 2 3 4 sralem ${⊢}\top \to {E}\left({ℂ}_{\mathrm{fld}}\right)={E}\left(\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)$
29 28 mptru ${⊢}{E}\left({ℂ}_{\mathrm{fld}}\right)={E}\left(\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\right)$
30 1 fveq2i ${⊢}{E}\left({C}\right)={E}\left(\mathrm{subringAlg}\left({ℂ}_{\mathrm{fld}}\right)\left(ℝ\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left({x}\in ℂ,{y}\in ℂ⟼{x}\stackrel{‾}{{y}}\right)⟩\right)$
31 22 29 30 3eqtr4i ${⊢}{E}\left({ℂ}_{\mathrm{fld}}\right)={E}\left({C}\right)$