Step | Hyp | Ref
| Expression |
1 | | cpmatsrngpmat.s |
. . . . . 6
ConstPolyMat |
2 | | cpmatsrngpmat.p |
. . . . . 6
Poly1 |
3 | | cpmatsrngpmat.c |
. . . . . 6
Mat |
4 | | eqid 2622 |
. . . . . 6
|
5 | | eqid 2622 |
. . . . . 6
|
6 | | eqid 2622 |
. . . . . 6
algSc algSc |
7 | 1, 2, 3, 4, 5, 6 | cpmatelimp2 20519 |
. . . . 5
algSc |
8 | 1, 2, 3, 4, 5, 6 | cpmatelimp2 20519 |
. . . . . . 7
algSc |
9 | | r19.26-2 3065 |
. . . . . . . . . . . . . 14
algSc
algSc
algSc
algSc |
10 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
11 | 5, 10 | ringacl 18578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
12 | 11 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
13 | 2 | ply1sca 19623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Scalar |
14 | 13 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Scalar |
15 | 14 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Scalar |
16 | 15 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Scalar |
17 | 16 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Scalar
|
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar
|
19 | 12, 18 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Scalar |
20 | 19 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Scalar |
21 | 20 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Scalar |
22 | 21 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Scalar |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc
algSc Scalar |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Scalar
algSc algSc Scalar |
25 | 24 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Scalar
algSc algSc Scalar |
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc
algSc Scalar algSc algSc Scalar |
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
28 | 27 | ancomd 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
29 | 28 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
30 | 29 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
algSc
algSc
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
33 | 3, 4, 31, 32 | matplusgcell 20239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
algSc
algSc |
35 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
algSc
algSc
algSc algSc |
36 | 35 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
algSc
algSc
algSc algSc |
37 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar Scalar |
38 | 2 | ply1ring 19618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
39 | 38 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
40 | 2 | ply1lmod 19622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
41 | 40 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
42 | 6, 37, 39, 41 | asclghm 19338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
algSc Scalar |
43 | 13 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
Scalar |
44 | 43 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Scalar |
45 | 44 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Scalar |
46 | 45 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Scalar |
47 | 46 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Scalar |
48 | 47 | adantrd 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar |
49 | 48 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Scalar |
50 | 13 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Scalar |
51 | 50 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Scalar |
52 | 51 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Scalar |
53 | 52 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Scalar |
54 | 53 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar |
55 | 54 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Scalar |
56 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar Scalar |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Scalar Scalar |
58 | 56, 57, 32 | ghmlin 17665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
algSc Scalar
Scalar
Scalar algSc
Scalar algSc
algSc |
59 | 42, 49, 55, 58 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
algSc
Scalar algSc
algSc |
60 | 59 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
algSc algSc algSc Scalar |
61 | 36, 60 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
algSc
algSc algSc
Scalar |
62 | 34, 61 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
algSc
algSc algSc Scalar |
63 | 23, 26, 62 | rspcedvd 3317 |
. . . . . . . . . . . . . . . . . . . . . 22
algSc
algSc algSc |
64 | 63 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
algSc algSc algSc |
65 | 64 | expd 452 |
. . . . . . . . . . . . . . . . . . . 20
algSc algSc
algSc |
66 | 65 | anassrs 680 |
. . . . . . . . . . . . . . . . . . 19
algSc algSc
algSc |
67 | 66 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . 18
algSc
algSc
algSc |
68 | 67 | com23 86 |
. . . . . . . . . . . . . . . . 17
algSc
algSc algSc |
69 | 68 | rexlimdva 3031 |
. . . . . . . . . . . . . . . 16
algSc algSc algSc |
70 | 69 | impd 447 |
. . . . . . . . . . . . . . 15
algSc
algSc
algSc |
71 | 70 | ralimdvva 2964 |
. . . . . . . . . . . . . 14
algSc
algSc
algSc |
72 | 9, 71 | syl5bir 233 |
. . . . . . . . . . . . 13
algSc
algSc
algSc |
73 | 72 | expd 452 |
. . . . . . . . . . . 12
algSc algSc
algSc |
74 | 73 | expr 643 |
. . . . . . . . . . 11
algSc algSc
algSc |
75 | 74 | impd 447 |
. . . . . . . . . 10
algSc algSc
algSc |
76 | 75 | ex 450 |
. . . . . . . . 9
algSc algSc
algSc |
77 | 76 | com34 91 |
. . . . . . . 8
algSc
algSc
algSc |
78 | 77 | impd 447 |
. . . . . . 7
algSc
algSc
algSc |
79 | 8, 78 | syld 47 |
. . . . . 6
algSc
algSc |
80 | 79 | com23 86 |
. . . . 5
algSc
algSc |
81 | 7, 80 | syld 47 |
. . . 4
algSc |
82 | 81 | imp32 449 |
. . 3
algSc |
83 | | simpl 473 |
. . . . 5
|
84 | 83 | adantr 481 |
. . . 4
|
85 | | simpr 477 |
. . . . 5
|
86 | 85 | adantr 481 |
. . . 4
|
87 | 2, 3 | pmatring 20498 |
. . . . . 6
|
88 | 87 | adantr 481 |
. . . . 5
|
89 | | simpl 473 |
. . . . . . . 8
|
90 | 89 | anim2i 593 |
. . . . . . 7
|
91 | | df-3an 1039 |
. . . . . . 7
|
92 | 90, 91 | sylibr 224 |
. . . . . 6
|
93 | 1, 2, 3, 4 | cpmatpmat 20515 |
. . . . . 6
|
94 | 92, 93 | syl 17 |
. . . . 5
|
95 | | simpr 477 |
. . . . . . . 8
|
96 | 95 | anim2i 593 |
. . . . . . 7
|
97 | | df-3an 1039 |
. . . . . . 7
|
98 | 96, 97 | sylibr 224 |
. . . . . 6
|
99 | 1, 2, 3, 4 | cpmatpmat 20515 |
. . . . . 6
|
100 | 98, 99 | syl 17 |
. . . . 5
|
101 | 4, 31 | ringacl 18578 |
. . . . 5
|
102 | 88, 94, 100, 101 | syl3anc 1326 |
. . . 4
|
103 | 1, 2, 3, 4, 5, 6 | cpmatel2 20518 |
. . . 4
algSc |
104 | 84, 86, 102, 103 | syl3anc 1326 |
. . 3
algSc |
105 | 82, 104 | mpbird 247 |
. 2
|
106 | 105 | ralrimivva 2971 |
1
|