Step |
Hyp |
Ref |
Expression |
1 |
|
ply1mulgsum.p |
|- P = ( Poly1 ` R ) |
2 |
|
ply1mulgsum.b |
|- B = ( Base ` P ) |
3 |
|
ply1mulgsum.a |
|- A = ( coe1 ` K ) |
4 |
|
ply1mulgsum.c |
|- C = ( coe1 ` L ) |
5 |
|
ply1mulgsum.x |
|- X = ( var1 ` R ) |
6 |
|
ply1mulgsum.pm |
|- .X. = ( .r ` P ) |
7 |
|
ply1mulgsum.sm |
|- .x. = ( .s ` P ) |
8 |
|
ply1mulgsum.rm |
|- .* = ( .r ` R ) |
9 |
|
ply1mulgsum.m |
|- M = ( mulGrp ` P ) |
10 |
|
ply1mulgsum.e |
|- .^ = ( .g ` M ) |
11 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
12 |
3 2 1 11
|
coe1ae0 |
|- ( K e. B -> E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) |
13 |
12
|
3ad2ant2 |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) |
14 |
4 2 1 11
|
coe1ae0 |
|- ( L e. B -> E. a e. NN0 A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) |
15 |
14
|
3ad2ant3 |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. a e. NN0 A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) |
16 |
|
nn0addcl |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( a + b ) e. NN0 ) |
17 |
16
|
adantr |
|- ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( a + b ) e. NN0 ) |
18 |
17
|
adantr |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) -> ( a + b ) e. NN0 ) |
19 |
|
breq1 |
|- ( s = ( a + b ) -> ( s < n <-> ( a + b ) < n ) ) |
20 |
19
|
imbi1d |
|- ( s = ( a + b ) -> ( ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) <-> ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
21 |
20
|
ralbidv |
|- ( s = ( a + b ) -> ( A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) <-> A. n e. NN0 ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
22 |
21
|
adantl |
|- ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) /\ s = ( a + b ) ) -> ( A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) <-> A. n e. NN0 ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
23 |
|
r19.26 |
|- ( A. n e. NN0 ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) <-> ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) |
24 |
|
nn0cn |
|- ( a e. NN0 -> a e. CC ) |
25 |
24
|
adantl |
|- ( ( b e. NN0 /\ a e. NN0 ) -> a e. CC ) |
26 |
|
nn0cn |
|- ( b e. NN0 -> b e. CC ) |
27 |
26
|
adantr |
|- ( ( b e. NN0 /\ a e. NN0 ) -> b e. CC ) |
28 |
25 27
|
addcomd |
|- ( ( b e. NN0 /\ a e. NN0 ) -> ( a + b ) = ( b + a ) ) |
29 |
28
|
3adant3 |
|- ( ( b e. NN0 /\ a e. NN0 /\ n e. NN0 ) -> ( a + b ) = ( b + a ) ) |
30 |
29
|
breq1d |
|- ( ( b e. NN0 /\ a e. NN0 /\ n e. NN0 ) -> ( ( a + b ) < n <-> ( b + a ) < n ) ) |
31 |
|
nn0sumltlt |
|- ( ( b e. NN0 /\ a e. NN0 /\ n e. NN0 ) -> ( ( b + a ) < n -> a < n ) ) |
32 |
30 31
|
sylbid |
|- ( ( b e. NN0 /\ a e. NN0 /\ n e. NN0 ) -> ( ( a + b ) < n -> a < n ) ) |
33 |
32
|
3expia |
|- ( ( b e. NN0 /\ a e. NN0 ) -> ( n e. NN0 -> ( ( a + b ) < n -> a < n ) ) ) |
34 |
33
|
ancoms |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( n e. NN0 -> ( ( a + b ) < n -> a < n ) ) ) |
35 |
34
|
adantr |
|- ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( n e. NN0 -> ( ( a + b ) < n -> a < n ) ) ) |
36 |
35
|
imp |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a + b ) < n -> a < n ) ) |
37 |
36
|
imim1d |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( ( a + b ) < n -> ( C ` n ) = ( 0g ` R ) ) ) ) |
38 |
37
|
com23 |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a + b ) < n -> ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( C ` n ) = ( 0g ` R ) ) ) ) |
39 |
38
|
imp |
|- ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( a + b ) < n ) -> ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( C ` n ) = ( 0g ` R ) ) ) |
40 |
|
nn0sumltlt |
|- ( ( a e. NN0 /\ b e. NN0 /\ n e. NN0 ) -> ( ( a + b ) < n -> b < n ) ) |
41 |
40
|
3expia |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( n e. NN0 -> ( ( a + b ) < n -> b < n ) ) ) |
42 |
41
|
adantr |
|- ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( n e. NN0 -> ( ( a + b ) < n -> b < n ) ) ) |
43 |
42
|
imp |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a + b ) < n -> b < n ) ) |
44 |
43
|
imim1d |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( ( a + b ) < n -> ( A ` n ) = ( 0g ` R ) ) ) ) |
45 |
44
|
com23 |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a + b ) < n -> ( ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( A ` n ) = ( 0g ` R ) ) ) ) |
46 |
45
|
imp |
|- ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( a + b ) < n ) -> ( ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( A ` n ) = ( 0g ` R ) ) ) |
47 |
39 46
|
anim12d |
|- ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( a + b ) < n ) -> ( ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> ( ( C ` n ) = ( 0g ` R ) /\ ( A ` n ) = ( 0g ` R ) ) ) ) |
48 |
47
|
imp |
|- ( ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( a + b ) < n ) /\ ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) -> ( ( C ` n ) = ( 0g ` R ) /\ ( A ` n ) = ( 0g ` R ) ) ) |
49 |
48
|
ancomd |
|- ( ( ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) /\ ( a + b ) < n ) /\ ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) |
50 |
49
|
exp31 |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( a + b ) < n -> ( ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
51 |
50
|
com23 |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ n e. NN0 ) -> ( ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
52 |
51
|
ralimdva |
|- ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( A. n e. NN0 ( ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> A. n e. NN0 ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
53 |
23 52
|
syl5bir |
|- ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) -> ( ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> A. n e. NN0 ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
54 |
53
|
imp |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) -> A. n e. NN0 ( ( a + b ) < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) |
55 |
18 22 54
|
rspcedvd |
|- ( ( ( ( a e. NN0 /\ b e. NN0 ) /\ ( R e. Ring /\ K e. B /\ L e. B ) ) /\ ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) |
56 |
55
|
exp31 |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
57 |
56
|
com23 |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
58 |
57
|
expd |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) ) |
59 |
58
|
com34 |
|- ( ( a e. NN0 /\ b e. NN0 ) -> ( A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) ) |
60 |
59
|
impancom |
|- ( ( a e. NN0 /\ A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) -> ( b e. NN0 -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) ) |
61 |
60
|
com14 |
|- ( A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( b e. NN0 -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( ( a e. NN0 /\ A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) ) |
62 |
61
|
impcom |
|- ( ( b e. NN0 /\ A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( ( a e. NN0 /\ A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
63 |
62
|
rexlimiva |
|- ( E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( ( a e. NN0 /\ A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
64 |
63
|
com13 |
|- ( ( a e. NN0 /\ A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
65 |
64
|
rexlimiva |
|- ( E. a e. NN0 A. n e. NN0 ( a < n -> ( C ` n ) = ( 0g ` R ) ) -> ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) ) |
66 |
15 65
|
mpcom |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( E. b e. NN0 A. n e. NN0 ( b < n -> ( A ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) ) |
67 |
13 66
|
mpd |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( ( A ` n ) = ( 0g ` R ) /\ ( C ` n ) = ( 0g ` R ) ) ) ) |