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