Theorem cchhllem

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

	Ref	Expression
Hypotheses	cchhl.c	⊢ 𝐶 = ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ )
	cchhllem.2	⊢ 𝐸 = Slot 𝑁
	cchhllem.3	⊢ 𝑁 ∈ ℕ
	cchhllem.4	⊢ ( 𝑁 < 5 ∨ 8 < 𝑁 )
Assertion	cchhllem	⊢ ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		cchhl.c	⊢ 𝐶 = ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ )
2		cchhllem.2	⊢ 𝐸 = Slot 𝑁
3		cchhllem.3	⊢ 𝑁 ∈ ℕ
4		cchhllem.4	⊢ ( 𝑁 < 5 ∨ 8 < 𝑁 )
5	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
6		5lt8	⊢ 5 < 8
7	3	nnrei	⊢ 𝑁 ∈ ℝ
8		5re	⊢ 5 ∈ ℝ
9		8re	⊢ 8 ∈ ℝ
10	7 8 9	lttri	⊢ ( ( 𝑁 < 5 ∧ 5 < 8 ) → 𝑁 < 8 )
11	6 10	mpan2	⊢ ( 𝑁 < 5 → 𝑁 < 8 )
12	7 9	ltnei	⊢ ( 𝑁 < 8 → 8 ≠ 𝑁 )
13	11 12	syl	⊢ ( 𝑁 < 5 → 8 ≠ 𝑁 )
14	13	necomd	⊢ ( 𝑁 < 5 → 𝑁 ≠ 8 )
15	9 7	ltnei	⊢ ( 8 < 𝑁 → 𝑁 ≠ 8 )
16	14 15	jaoi	⊢ ( ( 𝑁 < 5 ∨ 8 < 𝑁 ) → 𝑁 ≠ 8 )
17	4 16	ax-mp	⊢ 𝑁 ≠ 8
18	2 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
19		ipndx	⊢ ( ·𝑖 ‘ ndx ) = 8
20	18 19	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 𝑁 ≠ 8 )
21	17 20	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
22	5 21	setsnid	⊢ ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( 𝐸 ‘ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ ) )
23		eqidd	⊢ ( ⊤ → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
24		ax-resscn	⊢ ℝ ⊆ ℂ
25		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
26	24 25	sseqtri	⊢ ℝ ⊆ ( Base ‘ ℂfld )
27	26	a1i	⊢ ( ⊤ → ℝ ⊆ ( Base ‘ ℂfld ) )
28	23 27 2 3 4	sralem	⊢ ( ⊤ → ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
29	28	mptru	⊢ ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
30	1	fveq2i	⊢ ( 𝐸 ‘ 𝐶 ) = ( 𝐸 ‘ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · ( ∗ ‘ 𝑦 ) ) ) ⟩ ) )
31	22 29 30	3eqtr4i	⊢ ( 𝐸 ‘ ℂfld ) = ( 𝐸 ‘ 𝐶 )