Step | Hyp | Ref
| Expression |
1 | | cpmatsrngpmat.s |
. . . 4
ConstPolyMat |
2 | | cpmatsrngpmat.p |
. . . 4
Poly1 |
3 | | cpmatsrngpmat.c |
. . . 4
Mat |
4 | | eqid 2622 |
. . . 4
|
5 | 1, 2, 3, 4 | cpmatelimp 20517 |
. . 3
coe1 |
6 | 1, 2, 3, 4 | cpmatelimp 20517 |
. . . . . . . 8
coe1 |
7 | 6 | adantr 481 |
. . . . . . 7
coe1 |
8 | | ralcom 3098 |
. . . . . . . . . . . . . . . 16
coe1
coe1 |
9 | | r19.26-2 3065 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1
coe1 coe1 |
10 | | ralcom 3098 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1
coe1 coe1 |
11 | 9, 10 | bitr3i 266 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1
coe1 coe1 |
12 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
13 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
coe1 coe1 |
14 | 12, 13 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
coe1 coe1 |
15 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
17 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
18 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
19 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
21 | 3, 16, 4, 17, 18, 20 | matecld 20232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
22 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
23 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
25 | 3, 16, 4, 18, 22, 24 | matecld 20232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
26 | 15, 21, 25 | jca32 558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
27 | 26 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
coe1 coe1
|
28 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
29 | 28 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
coe1 coe1 |
30 | 29 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
coe1 coe1 |
31 | 30 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
coe1 coe1 |
32 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
|
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
coe1 coe1 |
34 | 33 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
coe1 coe1 |
35 | 34 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
coe1 coe1 |
36 | 31, 35 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
coe1 coe1 coe1 coe1 |
37 | 36 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
coe1 coe1 coe1 coe1 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
coe1 coe1 coe1 coe1 |
39 | 38 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
coe1 coe1 coe1 coe1 |
40 | 39 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
coe1 coe1
coe1 coe1 |
41 | 40 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
coe1 coe1 coe1 coe1 |
42 | 41 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
coe1 coe1
coe1 coe1 |
43 | 42 | impancom 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
coe1 coe1
coe1 coe1 |
44 | 43 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
coe1 coe1
coe1 coe1 |
45 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
46 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
47 | 2, 16, 45, 46 | cply1mul 19664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
coe1 coe1
coe1 |
48 | 27, 44, 47 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
coe1 coe1
coe1 |
49 | 48 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
coe1 coe1
coe1 |
50 | 49 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
coe1 coe1
coe1 |
51 | 50 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
coe1 coe1 coe1 |
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
coe1 coe1 g coe1 g |
53 | | ringmnd 18556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
54 | 53 | anim2i 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
55 | 54 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
56 | 45 | gsumz 17374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
g |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
g |
58 | 57 | ad4antr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
coe1 coe1 g |
59 | 52, 58 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
coe1 coe1 g coe1 |
60 | 59 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
coe1 coe1
g coe1 |
61 | 14, 60 | ralrimi 2957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1
g coe1 |
62 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
63 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
65 | 2 | ply1ring 19618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
66 | 65 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
67 | 16, 46 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
68 | 66, 21, 25, 67 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
69 | 68 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
71 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
72 | 2, 16, 62, 64, 70, 71 | coe1fzgsumd 19672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
coe1 g g coe1 |
73 | 72 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
coe1 g
g coe1 |
74 | 73 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
coe1 g
g coe1 |
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coe1 coe1 coe1 g
g coe1 |
76 | 61, 75 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
coe1 coe1 coe1 g |
77 | 76 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
coe1 coe1
coe1 g |
78 | 11, 77 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . 21
coe1 coe1
coe1 g |
79 | 78 | expd 452 |
. . . . . . . . . . . . . . . . . . . 20
coe1
coe1 coe1 g |
80 | 79 | expr 643 |
. . . . . . . . . . . . . . . . . . 19
coe1
coe1 coe1 g |
81 | 80 | com23 86 |
. . . . . . . . . . . . . . . . . 18
coe1
coe1 coe1 g |
82 | 81 | imp31 448 |
. . . . . . . . . . . . . . . . 17
coe1
coe1 coe1 g |
83 | 82 | ralimdva 2962 |
. . . . . . . . . . . . . . . 16
coe1
coe1
coe1 g |
84 | 8, 83 | syl5bi 232 |
. . . . . . . . . . . . . . 15
coe1
coe1
coe1 g |
85 | 84 | ex 450 |
. . . . . . . . . . . . . 14
coe1
coe1
coe1 g |
86 | 85 | com23 86 |
. . . . . . . . . . . . 13
coe1
coe1
coe1 g |
87 | 86 | impancom 456 |
. . . . . . . . . . . 12
coe1
coe1
coe1 g |
88 | 87 | imp 445 |
. . . . . . . . . . 11
coe1
coe1
coe1 g |
89 | 88 | ralimdva 2962 |
. . . . . . . . . 10
coe1
coe1
coe1 g |
90 | 89 | ex 450 |
. . . . . . . . 9
coe1
coe1
coe1 g |
91 | 90 | expr 643 |
. . . . . . . 8
coe1
coe1
coe1 g |
92 | 91 | impd 447 |
. . . . . . 7
coe1 coe1
coe1 g |
93 | 7, 92 | syld 47 |
. . . . . 6
coe1
coe1 g |
94 | 93 | com23 86 |
. . . . 5
coe1
coe1 g |
95 | 94 | ex 450 |
. . . 4
coe1
coe1 g |
96 | 95 | impd 447 |
. . 3
coe1
coe1 g |
97 | 5, 96 | syld 47 |
. 2
coe1 g |
98 | 97 | imp32 449 |
1
coe1 g |