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\bar{y}\right)⟩$$
	cchhllem.2	$$⊢E=\mathrm{Slot}N$$
	cchhllem.3	$$⊢N\in \mathbb{N}$$
	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\bar{y}\right)⟩$$
2		cchhllem.2	$$⊢E=\mathrm{Slot}N$$
3		cchhllem.3	$$⊢N\in \mathbb{N}$$
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)\leftrightarrow 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\bar{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\bar{y}\right)⟩\right)$$
31	22 29 30	3eqtr4i	$$⊢E\left({ℂ}_{\mathrm{fld}}\right)=E\left(C\right)$$