Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmattomply1f1lem Structured version   Unicode version

Theorem pmattomply1f1lem 31257
 Description: Lemma for pmattomply1f1 31269. (Contributed by AV, 14-Oct-2019.)
Hypotheses
Ref Expression
pmattomply1.p Poly1
pmattomply1.c Mat
pmattomply1.b
pmattomply1.f coe1
pmattomply1.m
pmattomply1.e .gmulGrp
pmattomply1.x var1
pmattomply1.a Mat
pmattomply1.q Poly1
pmattomply1.l
Assertion
Ref Expression
pmattomply1f1lem coe1 g
Distinct variable groups:   ,,,,   ,,,   ,,,   ,,   ,,,   ,,,   ,   ,,,,   ,   ,   ,   ,,,,   ,   ,   ,
Allowed substitution hints:   ()   (,,)   (,,)   ()   (,,)   ()   (,,)   (,,)   (,,)   (,,,)

Proof of Theorem pmattomply1f1lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pmattomply1.q . . 3 Poly1
2 pmattomply1.l . . 3
3 pmattomply1.x . . 3 var1
4 pmattomply1.e . . 3 .gmulGrp
5 pmattomply1.a . . . . 5 Mat
65matrng 18442 . . . 4
8 eqid 2451 . . 3
9 pmattomply1.m . . 3
10 eqid 2451 . . 3
11 simpll 753 . . . . 5
12 simprl 755 . . . . . 6
1312anim1i 568 . . . . 5
14 pmattomply1.p . . . . . 6 Poly1
15 pmattomply1.c . . . . . 6 Mat
16 pmattomply1.b . . . . . 6
17 pmattomply1.f . . . . . . 7 coe1
18 oveq 6198 . . . . . . . . . . . 12
1918fveq2d 5795 . . . . . . . . . . 11 coe1 coe1
2019fveq1d 5793 . . . . . . . . . 10 coe1 coe1
2120mpt2eq3dv 6253 . . . . . . . . 9 coe1 coe1
22 fveq2 5791 . . . . . . . . . 10 coe1 coe1
2322mpt2eq3dv 6253 . . . . . . . . 9 coe1 coe1
2421, 23cbvmpt2v 6267 . . . . . . . 8 coe1 coe1
25 oveq 6198 . . . . . . . . . . . 12
2625fveq2d 5795 . . . . . . . . . . 11 coe1 coe1
2726fveq1d 5793 . . . . . . . . . 10 coe1 coe1
2827mpt2eq3dv 6253 . . . . . . . . 9 coe1 coe1
29 fveq2 5791 . . . . . . . . . 10 coe1 coe1
3029mpt2eq3dv 6253 . . . . . . . . 9 coe1 coe1
3128, 30cbvmpt2v 6267 . . . . . . . 8 coe1 coe1
3224, 31eqtri 2480 . . . . . . 7 coe1 coe1
3317, 32eqtri 2480 . . . . . 6 coe1
3414, 15, 16, 33, 5, 8pmatcollpw1lem2 31226 . . . . 5
3511, 13, 34syl2anc 661 . . . 4
3635ralrimiva 2822 . . 3
37 simpll 753 . . . 4
38 simpr 461 . . . . 5
3938adantr 465 . . . 4
4014, 15, 16, 17, 5pmatcollpwfsupp 31231 . . . 4 finSupp
4137, 39, 12, 40syl3anc 1219 . . 3 finSupp
42 simprr 756 . . 3
431, 2, 3, 4, 7, 8, 9, 10, 36, 41, 42gsummoncoe1 30987 . 2 coe1 g
44 csbov2g 6228 . . 3