Metamath Proof Explorer


Theorem ply1mulgsumlem1

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

Ref Expression
Hypotheses ply1mulgsum.p P = Poly 1 R
ply1mulgsum.b B = Base P
ply1mulgsum.a A = coe 1 K
ply1mulgsum.c C = coe 1 L
ply1mulgsum.x X = var 1 R
ply1mulgsum.pm × ˙ = P
ply1mulgsum.sm · ˙ = P
ply1mulgsum.rm ˙ = R
ply1mulgsum.m M = mulGrp P
ply1mulgsum.e × ˙ = M
Assertion ply1mulgsumlem1 R Ring K B L B s 0 n 0 s < n A n = 0 R C n = 0 R

Proof

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