Metamath Proof Explorer

Theorem cchhllemOLD

Description: Obsolete version of cchhllem as of 29-Oct-2024. Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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