Metamath Proof Explorer

Theorem deg1gprod

Description: Degree multiplication is a homomorphism. (Contributed by metakunt, 6-May-2025)

Ref Expression
Hypotheses deg1gprod.1 
|- ( ph -> R e. IDomn )
deg1gprod.2 
|- ( ph -> N e. Fin )
deg1gprod.3 
|- ( ph -> A. x e. N ( C e. ( Base ` ( Poly1 ` R ) ) /\ C =/= ( 0g ` ( Poly1 ` R ) ) ) )
Assertion deg1gprod 
|- ( ph -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) = sum_ n e. N ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 deg1gprod.1 
 |-  ( ph -> R e. IDomn )
2 deg1gprod.2 
 |-  ( ph -> N e. Fin )
3 deg1gprod.3 
 |-  ( ph -> A. x e. N ( C e. ( Base ` ( Poly1 ` R ) ) /\ C =/= ( 0g ` ( Poly1 ` R ) ) ) )
4 mpteq1 
 |-  ( a = (/) -> ( x e. a |-> C ) = ( x e. (/) |-> C ) )
5 4 oveq2d 
 |-  ( a = (/) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) )
6 5 fveq2d 
 |-  ( a = (/) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) )
7 sumeq1 
 |-  ( a = (/) -> sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
8 6 7 eqeq12d 
 |-  ( a = (/) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) <-> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) ) )
9 6 breq2d 
 |-  ( a = (/) -> ( 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) <-> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) ) )
10 8 9 anbi12d 
 |-  ( a = (/) -> ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) ) <-> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) ) ) )
11 mpteq1 
 |-  ( a = b -> ( x e. a |-> C ) = ( x e. b |-> C ) )
12 11 oveq2d 
 |-  ( a = b -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) )
13 12 fveq2d 
 |-  ( a = b -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) )
14 sumeq1 
 |-  ( a = b -> sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
15 13 14 eqeq12d 
 |-  ( a = b -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) <-> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) ) )
16 13 breq2d 
 |-  ( a = b -> ( 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) <-> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) )
17 15 16 anbi12d 
 |-  ( a = b -> ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) ) <-> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) )
18 mpteq1 
 |-  ( a = ( b u. { c } ) -> ( x e. a |-> C ) = ( x e. ( b u. { c } ) |-> C ) )
19 18 oveq2d 
 |-  ( a = ( b u. { c } ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) )
20 19 fveq2d 
 |-  ( a = ( b u. { c } ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) )
21 sumeq1 
 |-  ( a = ( b u. { c } ) -> sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
22 20 21 eqeq12d 
 |-  ( a = ( b u. { c } ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) <-> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) ) )
23 20 breq2d 
 |-  ( a = ( b u. { c } ) -> ( 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) <-> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) ) )
24 22 23 anbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) ) <-> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) ) ) )
25 mpteq1 
 |-  ( a = N -> ( x e. a |-> C ) = ( x e. N |-> C ) )
26 25 oveq2d 
 |-  ( a = N -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) )
27 26 fveq2d 
 |-  ( a = N -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) )
28 sumeq1 
 |-  ( a = N -> sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = sum_ n e. N ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
29 27 28 eqeq12d 
 |-  ( a = N -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) <-> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) = sum_ n e. N ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) ) )
30 27 breq2d 
 |-  ( a = N -> ( 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) <-> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) ) )
31 29 30 anbi12d 
 |-  ( a = N -> ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) = sum_ n e. a ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. a |-> C ) ) ) ) <-> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) = sum_ n e. N ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) ) ) )
32 mpt0 
 |-  ( x e. (/) |-> C ) = (/)
33 32 a1i 
 |-  ( ph -> ( x e. (/) |-> C ) = (/) )
34 33 oveq2d 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum (/) ) )
35 eqid 
 |-  ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) )
36 35 gsum0 
 |-  ( ( mulGrp ` ( Poly1 ` R ) ) gsum (/) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) )
37 36 a1i 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum (/) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) )
38 34 37 eqtrd 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) )
39 38 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = ( ( deg1 ` R ) ` ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) ) )
40 1 idomringd 
 |-  ( ph -> R e. Ring )
41 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
42 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
43 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
44 eqid 
 |-  ( mulGrp ` ( Poly1 ` R ) ) = ( mulGrp ` ( Poly1 ` R ) )
45 eqid 
 |-  ( 1r ` ( Poly1 ` R ) ) = ( 1r ` ( Poly1 ` R ) )
46 44 45 ringidval 
 |-  ( 1r ` ( Poly1 ` R ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) )
47 46 eqcomi 
 |-  ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( 1r ` ( Poly1 ` R ) )
48 41 42 43 47 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) )
49 40 48 syl 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) )
50 49 eqcomd 
 |-  ( ph -> ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) )
51 50 fveq2d 
 |-  ( ph -> ( ( deg1 ` R ) ` ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) ) = ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) )
52 eqid 
 |-  ( Base ` R ) = ( Base ` R )
53 52 43 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
54 40 53 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
55 1 idomdomd 
 |-  ( ph -> R e. Domn )
56 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
57 55 56 syl 
 |-  ( ph -> R e. NzRing )
58 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
59 43 58 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
60 57 59 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
61 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
62 61 41 52 42 58 deg1scl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) = 0 )
63 40 54 60 62 syl3anc 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) = 0 )
64 51 63 eqtrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) ) ) = 0 )
65 39 64 eqtrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = 0 )
66 sum0 
 |-  sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = 0
67 66 eqcomi 
 |-  0 = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) )
68 67 a1i 
 |-  ( ph -> 0 = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
69 65 68 eqtrd 
 |-  ( ph -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
70 0red 
 |-  ( ph -> 0 e. RR )
71 70 leidd 
 |-  ( ph -> 0 <_ 0 )
72 65 eqcomd 
 |-  ( ph -> 0 = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) )
73 71 72 breqtrd 
 |-  ( ph -> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) )
74 69 73 jca 
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) = sum_ n e. (/) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. (/) |-> C ) ) ) ) )
75 nfcv 
 |-  F/_ y C
76 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
77 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
78 75 76 77 cbvmpt 
 |-  ( x e. ( b u. { c } ) |-> C ) = ( y e. ( b u. { c } ) |-> [_ y / x ]_ C )
79 78 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( x e. ( b u. { c } ) |-> C ) = ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) )
80 79 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) )
81 80 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) ) )
82 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` R ) ) )
83 eqid 
 |-  ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( +g ` ( mulGrp ` ( Poly1 ` R ) ) )
84 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
85 1 84 sylib 
 |-  ( ph -> ( R e. CRing /\ R e. Domn ) )
86 85 simpld 
 |-  ( ph -> R e. CRing )
87 41 ply1crng 
 |-  ( R e. CRing -> ( Poly1 ` R ) e. CRing )
88 86 87 syl 
 |-  ( ph -> ( Poly1 ` R ) e. CRing )
89 44 crngmgp 
 |-  ( ( Poly1 ` R ) e. CRing -> ( mulGrp ` ( Poly1 ` R ) ) e. CMnd )
90 88 89 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` R ) ) e. CMnd )
91 90 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( mulGrp ` ( Poly1 ` R ) ) e. CMnd )
92 91 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( mulGrp ` ( Poly1 ` R ) ) e. CMnd )
93 2 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> N e. Fin )
94 simplrl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> b C_ N )
95 93 94 ssfid 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> b e. Fin )
96 94 sselda 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> y e. N )
97 r19.26 
 |-  ( A. x e. N ( C e. ( Base ` ( Poly1 ` R ) ) /\ C =/= ( 0g ` ( Poly1 ` R ) ) ) <-> ( A. x e. N C e. ( Base ` ( Poly1 ` R ) ) /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) )
98 97 biimpi 
 |-  ( A. x e. N ( C e. ( Base ` ( Poly1 ` R ) ) /\ C =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( A. x e. N C e. ( Base ` ( Poly1 ` R ) ) /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) )
99 3 98 syl 
 |-  ( ph -> ( A. x e. N C e. ( Base ` ( Poly1 ` R ) ) /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) )
100 99 simpld 
 |-  ( ph -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
101 100 ad3antrrr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
102 rspcsbela 
 |-  ( ( y e. N /\ A. x e. N C e. ( Base ` ( Poly1 ` R ) ) ) -> [_ y / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
103 96 101 102 syl2anc 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> [_ y / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
104 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
105 44 104 mgpbas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( mulGrp ` ( Poly1 ` R ) ) )
106 103 105 eleqtrdi 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> [_ y / x ]_ C e. ( Base ` ( mulGrp ` ( Poly1 ` R ) ) ) )
107 eldifi 
 |-  ( c e. ( N \ b ) -> c e. N )
108 107 adantl 
 |-  ( ( b C_ N /\ c e. ( N \ b ) ) -> c e. N )
109 108 adantl 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> c e. N )
110 109 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> c e. N )
111 eldifn 
 |-  ( c e. ( N \ b ) -> -. c e. b )
112 111 adantl 
 |-  ( ( b C_ N /\ c e. ( N \ b ) ) -> -. c e. b )
113 112 adantl 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> -. c e. b )
114 113 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> -. c e. b )
115 100 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
116 rspcsbela 
 |-  ( ( c e. N /\ A. x e. N C e. ( Base ` ( Poly1 ` R ) ) ) -> [_ c / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
117 110 115 116 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> [_ c / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
118 117 105 eleqtrdi 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> [_ c / x ]_ C e. ( Base ` ( mulGrp ` ( Poly1 ` R ) ) ) )
119 csbeq1 
 |-  ( y = c -> [_ y / x ]_ C = [_ c / x ]_ C )
120 82 83 92 95 106 110 114 118 119 gsumunsn 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) = ( ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) [_ c / x ]_ C ) )
121 120 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) ) = ( ( deg1 ` R ) ` ( ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) [_ c / x ]_ C ) ) )
122 eqid 
 |-  ( .r ` ( Poly1 ` R ) ) = ( .r ` ( Poly1 ` R ) )
123 44 122 mgpplusg 
 |-  ( .r ` ( Poly1 ` R ) ) = ( +g ` ( mulGrp ` ( Poly1 ` R ) ) )
124 123 eqcomi 
 |-  ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( .r ` ( Poly1 ` R ) )
125 eqid 
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
126 55 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> R e. Domn )
127 126 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> R e. Domn )
128 103 ralrimiva 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> A. y e. b [_ y / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
129 105 92 95 128 gsummptcl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) e. ( Base ` ( Poly1 ` R ) ) )
130 41 ply1idom 
 |-  ( R e. IDomn -> ( Poly1 ` R ) e. IDomn )
131 1 130 syl 
 |-  ( ph -> ( Poly1 ` R ) e. IDomn )
132 131 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( Poly1 ` R ) e. IDomn )
133 132 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( Poly1 ` R ) e. IDomn )
134 99 simprd 
 |-  ( ph -> A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) )
135 134 ad3antrrr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) )
136 rspcsbnea 
 |-  ( ( y e. N /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) -> [_ y / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
137 96 135 136 syl2anc 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) /\ y e. b ) -> [_ y / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
138 44 133 95 103 137 idomnnzgmulnz 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) =/= ( 0g ` ( Poly1 ` R ) ) )
139 134 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) )
140 rspcsbnea 
 |-  ( ( c e. N /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) -> [_ c / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
141 110 139 140 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> [_ c / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
142 61 41 104 124 125 127 129 138 117 141 deg1mul 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) [_ c / x ]_ C ) ) = ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) )
143 75 76 77 cbvmpt 
 |-  ( x e. b |-> C ) = ( y e. b |-> [_ y / x ]_ C )
144 143 eqcomi 
 |-  ( y e. b |-> [_ y / x ]_ C ) = ( x e. b |-> C )
145 144 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( y e. b |-> [_ y / x ]_ C ) = ( x e. b |-> C ) )
146 145 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) )
147 146 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ) = ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) )
148 147 oveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) = ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) )
149 simpl 
 |-  ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
150 149 adantl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
151 150 oveq1d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) = ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) )
152 nfv 
 |-  F/ n ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) )
153 nfcv 
 |-  F/_ n ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) )
154 2 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> N e. Fin )
155 simprl 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> b C_ N )
156 154 155 ssfid 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> b e. Fin )
157 75 76 77 cbvmpt 
 |-  ( x e. N |-> C ) = ( y e. N |-> [_ y / x ]_ C )
158 157 fveq1i 
 |-  ( ( x e. N |-> C ) ` n ) = ( ( y e. N |-> [_ y / x ]_ C ) ` n )
159 158 a1i 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( x e. N |-> C ) ` n ) = ( ( y e. N |-> [_ y / x ]_ C ) ` n ) )
160 159 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = ( ( deg1 ` R ) ` ( ( y e. N |-> [_ y / x ]_ C ) ` n ) ) )
161 eqidd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( y e. N |-> [_ y / x ]_ C ) = ( y e. N |-> [_ y / x ]_ C ) )
162 simpr 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) /\ y = n ) -> y = n )
163 162 csbeq1d 
 |-  ( ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) /\ y = n ) -> [_ y / x ]_ C = [_ n / x ]_ C )
164 155 sselda 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> n e. N )
165 100 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
166 165 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
167 rspcsbela 
 |-  ( ( n e. N /\ A. x e. N C e. ( Base ` ( Poly1 ` R ) ) ) -> [_ n / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
168 164 166 167 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> [_ n / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
169 161 163 164 168 fvmptd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( y e. N |-> [_ y / x ]_ C ) ` n ) = [_ n / x ]_ C )
170 169 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` ( ( y e. N |-> [_ y / x ]_ C ) ` n ) ) = ( ( deg1 ` R ) ` [_ n / x ]_ C ) )
171 40 adantr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> R e. Ring )
172 171 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> R e. Ring )
173 134 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) )
174 rspcsbnea 
 |-  ( ( n e. N /\ A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) ) -> [_ n / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
175 164 173 174 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> [_ n / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
176 61 41 125 104 deg1nn0cl 
 |-  ( ( R e. Ring /\ [_ n / x ]_ C e. ( Base ` ( Poly1 ` R ) ) /\ [_ n / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( ( deg1 ` R ) ` [_ n / x ]_ C ) e. NN0 )
177 172 168 175 176 syl3anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` [_ n / x ]_ C ) e. NN0 )
178 170 177 eqeltrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` ( ( y e. N |-> [_ y / x ]_ C ) ` n ) ) e. NN0 )
179 160 178 eqeltrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) e. NN0 )
180 179 nn0cnd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ n e. b ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) e. CC )
181 2fveq3 
 |-  ( n = c -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) )
182 109 165 116 syl2anc 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> [_ c / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
183 eqid 
 |-  ( x e. N |-> C ) = ( x e. N |-> C )
184 183 fvmpts 
 |-  ( ( c e. N /\ [_ c / x ]_ C e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( x e. N |-> C ) ` c ) = [_ c / x ]_ C )
185 109 182 184 syl2anc 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( x e. N |-> C ) ` c ) = [_ c / x ]_ C )
186 185 fveq2d 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) = ( ( deg1 ` R ) ` [_ c / x ]_ C ) )
187 108 134 140 syl2anr 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> [_ c / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
188 61 41 125 104 deg1nn0cl 
 |-  ( ( R e. Ring /\ [_ c / x ]_ C e. ( Base ` ( Poly1 ` R ) ) /\ [_ c / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( ( deg1 ` R ) ` [_ c / x ]_ C ) e. NN0 )
189 171 182 187 188 syl3anc 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( deg1 ` R ) ` [_ c / x ]_ C ) e. NN0 )
190 186 189 eqeltrd 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) e. NN0 )
191 190 nn0cnd 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) e. CC )
192 152 153 156 109 113 180 181 191 fsumsplitsn 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) ) )
193 192 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) ) )
194 185 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( x e. N |-> C ) ` c ) = [_ c / x ]_ C )
195 194 fveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) = ( ( deg1 ` R ) ` [_ c / x ]_ C ) )
196 195 oveq2d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` c ) ) ) = ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) )
197 193 196 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) = ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) )
198 197 eqcomd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
199 151 198 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
200 148 199 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ) + ( ( deg1 ` R ) ` [_ c / x ]_ C ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
201 142 200 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. b |-> [_ y / x ]_ C ) ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) [_ c / x ]_ C ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
202 121 201 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
203 81 202 eqtrd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) )
204 171 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> R e. Ring )
205 110 snssd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> { c } C_ N )
206 94 205 unssd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( b u. { c } ) C_ N )
207 93 206 ssfid 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( b u. { c } ) e. Fin )
208 165 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
209 ssralv 
 |-  ( ( b u. { c } ) C_ N -> ( A. x e. N C e. ( Base ` ( Poly1 ` R ) ) -> A. x e. ( b u. { c } ) C e. ( Base ` ( Poly1 ` R ) ) ) )
210 206 209 syl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( A. x e. N C e. ( Base ` ( Poly1 ` R ) ) -> A. x e. ( b u. { c } ) C e. ( Base ` ( Poly1 ` R ) ) ) )
211 208 210 mpd 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> A. x e. ( b u. { c } ) C e. ( Base ` ( Poly1 ` R ) ) )
212 105 92 207 211 gsummptcl 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) e. ( Base ` ( Poly1 ` R ) ) )
213 78 oveq2i 
 |-  ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) )
214 213 a1i 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) = ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) )
215 109 snssd 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> { c } C_ N )
216 155 215 unssd 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( b u. { c } ) C_ N )
217 154 216 ssfid 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( b u. { c } ) e. Fin )
218 216 sselda 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ y e. ( b u. { c } ) ) -> y e. N )
219 165 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ y e. ( b u. { c } ) ) -> A. x e. N C e. ( Base ` ( Poly1 ` R ) ) )
220 218 219 102 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ y e. ( b u. { c } ) ) -> [_ y / x ]_ C e. ( Base ` ( Poly1 ` R ) ) )
221 134 ad2antrr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ y e. ( b u. { c } ) ) -> A. x e. N C =/= ( 0g ` ( Poly1 ` R ) ) )
222 218 221 136 syl2anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ y e. ( b u. { c } ) ) -> [_ y / x ]_ C =/= ( 0g ` ( Poly1 ` R ) ) )
223 44 132 217 220 222 idomnnzgmulnz 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( y e. ( b u. { c } ) |-> [_ y / x ]_ C ) ) =/= ( 0g ` ( Poly1 ` R ) ) )
224 214 223 eqnetrd 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) =/= ( 0g ` ( Poly1 ` R ) ) )
225 224 adantr 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) =/= ( 0g ` ( Poly1 ` R ) ) )
226 61 41 125 104 deg1nn0cl 
 |-  ( ( R e. Ring /\ ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) e. NN0 )
227 204 212 225 226 syl3anc 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) e. NN0 )
228 227 nn0ge0d 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) )
229 203 228 jca 
 |-  ( ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) /\ ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) ) )
230 229 ex 
 |-  ( ( ph /\ ( b C_ N /\ c e. ( N \ b ) ) ) -> ( ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) = sum_ n e. b ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. b |-> C ) ) ) ) -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) = sum_ n e. ( b u. { c } ) ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. ( b u. { c } ) |-> C ) ) ) ) ) )
231 10 17 24 31 74 230 2 findcard2d 
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) = sum_ n e. N ( ( deg1 ` R ) ` ( ( x e. N |-> C ) ` n ) ) /\ 0 <_ ( ( deg1 ` R ) ` ( ( mulGrp ` ( Poly1 ` R ) ) gsum ( x e. N |-> C ) ) ) ) )