Metamath Proof Explorer


Theorem ply1mulgsumlem1

Description: Lemma 1 for ply1mulgsum . (Contributed by AV, 19-Oct-2019)

Ref Expression
Hypotheses ply1mulgsum.p
|- P = ( Poly1 ` R )
ply1mulgsum.b
|- B = ( Base ` P )
ply1mulgsum.a
|- A = ( coe1 ` K )
ply1mulgsum.c
|- C = ( coe1 ` L )
ply1mulgsum.x
|- X = ( var1 ` R )
ply1mulgsum.pm
|- .X. = ( .r ` P )
ply1mulgsum.sm
|- .x. = ( .s ` P )
ply1mulgsum.rm
|- .* = ( .r ` R )
ply1mulgsum.m
|- M = ( mulGrp ` P )
ply1mulgsum.e
|- .^ = ( .g ` M )
Assertion ply1mulgsumlem1
|- ( ( 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 ) ) ) )

Proof

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 ) ) ) )