Theorem cchhllem

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

	Ref	Expression
Hypotheses	cchhl.c	|- C = ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. )
	cchhllem.2	|- E = Slot N
	cchhllem.3	|- N e. NN
	cchhllem.4	|- ( N < 5 \/ 8 < N )
Assertion	cchhllem	|- ( E ` CCfld ) = ( E ` C )

Proof

Step	Hyp	Ref	Expression
1		cchhl.c	|- C = ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. )
2		cchhllem.2	|- E = Slot N
3		cchhllem.3	|- N e. NN
4		cchhllem.4	|- ( N < 5 \/ 8 < N )
5	2 3	ndxid	|- E = Slot ( E ` ndx )
6		5lt8	|- 5 < 8
7	3	nnrei	|- N e. RR
8		5re	|- 5 e. RR
9		8re	|- 8 e. RR
10	7 8 9	lttri	|- ( ( N < 5 /\ 5 < 8 ) -> N < 8 )
11	6 10	mpan2	|- ( N < 5 -> N < 8 )
12	7 9	ltnei	|- ( N < 8 -> 8 =/= N )
13	11 12	syl	|- ( N < 5 -> 8 =/= N )
14	13	necomd	|- ( N < 5 -> N =/= 8 )
15	9 7	ltnei	|- ( 8 < N -> N =/= 8 )
16	14 15	jaoi	|- ( ( N < 5 \/ 8 < N ) -> N =/= 8 )
17	4 16	ax-mp	|- N =/= 8
18	2 3	ndxarg	|- ( E ` ndx ) = N
19		ipndx	|- ( .i ` ndx ) = 8
20	18 19	neeq12i	|- ( ( E ` ndx ) =/= ( .i ` ndx ) <-> N =/= 8 )
21	17 20	mpbir	|- ( E ` ndx ) =/= ( .i ` ndx )
22	5 21	setsnid	|- ( E ` ( ( subringAlg ` CCfld ) ` RR ) ) = ( E ` ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. ) )
23		eqidd	|- ( T. -> ( ( subringAlg ` CCfld ) ` RR ) = ( ( subringAlg ` CCfld ) ` RR ) )
24		ax-resscn	|- RR C_ CC
25		cnfldbas	|- CC = ( Base ` CCfld )
26	24 25	sseqtri	|- RR C_ ( Base ` CCfld )
27	26	a1i	|- ( T. -> RR C_ ( Base ` CCfld ) )
28	23 27 2 3 4	sralem	|- ( T. -> ( E ` CCfld ) = ( E ` ( ( subringAlg ` CCfld ) ` RR ) ) )
29	28	mptru	|- ( E ` CCfld ) = ( E ` ( ( subringAlg ` CCfld ) ` RR ) )
30	1	fveq2i	|- ( E ` C ) = ( E ` ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. ) )
31	22 29 30	3eqtr4i	|- ( E ` CCfld ) = ( E ` C )