Metamath Proof Explorer

Theorem cchhllem

Description: Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019) (Revised by AV, 29-Oct-2024)

Ref Expression
Hypotheses cchhl.c 
|- C = ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. )
cchhllem.1 
|- E = Slot ( E ` ndx )
cchhllem.2 
|- ( Scalar ` ndx ) =/= ( E ` ndx )
cchhllem.3 
|- ( .s ` ndx ) =/= ( E ` ndx )
cchhllem.4 
|- ( .i ` ndx ) =/= ( E ` ndx )
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.1 
 |-  E = Slot ( E ` ndx )
3 cchhllem.2 
 |-  ( Scalar ` ndx ) =/= ( E ` ndx )
4 cchhllem.3 
 |-  ( .s ` ndx ) =/= ( E ` ndx )
5 cchhllem.4 
 |-  ( .i ` ndx ) =/= ( E ` ndx )
6 5 necomi 
 |-  ( E ` ndx ) =/= ( .i ` ndx )
7 2 6 setsnid 
 |-  ( E ` ( ( subringAlg ` CCfld ) ` RR ) ) = ( E ` ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. ) )
8 eqidd 
 |-  ( T. -> ( ( subringAlg ` CCfld ) ` RR ) = ( ( subringAlg ` CCfld ) ` RR ) )
9 ax-resscn 
 |-  RR C_ CC
10 cnfldbas 
 |-  CC = ( Base ` CCfld )
11 9 10 sseqtri 
 |-  RR C_ ( Base ` CCfld )
12 11 a1i 
 |-  ( T. -> RR C_ ( Base ` CCfld ) )
13 8 12 2 3 4 5 sralem 
 |-  ( T. -> ( E ` CCfld ) = ( E ` ( ( subringAlg ` CCfld ) ` RR ) ) )
14 13 mptru 
 |-  ( E ` CCfld ) = ( E ` ( ( subringAlg ` CCfld ) ` RR ) )
15 1 fveq2i 
 |-  ( E ` C ) = ( E ` ( ( ( subringAlg ` CCfld ) ` RR ) sSet <. ( .i ` ndx ) , ( x e. CC , y e. CC |-> ( x x. ( * ` y ) ) ) >. ) )
16 7 14 15 3eqtr4i 
 |-  ( E ` CCfld ) = ( E ` C )