Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
|
2 | | eqid 2622 |
. . 3
Scalar Scalar |
3 | | lincscm.r |
. . 3
Scalar |
4 | | eqid 2622 |
. . 3
|
5 | | eqid 2622 |
. . 3
|
6 | | lincscm.s |
. . 3
|
7 | | simp1l 1085 |
. . 3
finSupp Scalar |
8 | | simpr 477 |
. . . 4
|
9 | 8 | 3ad2ant1 1082 |
. . 3
finSupp Scalar |
10 | | simpr 477 |
. . . 4
|
11 | 10 | 3ad2ant2 1083 |
. . 3
finSupp Scalar |
12 | 7 | adantr 481 |
. . . 4
finSupp Scalar
|
13 | | elmapi 7879 |
. . . . . . . 8
|
14 | | ffvelrn 6357 |
. . . . . . . . 9
|
15 | 14 | ex 450 |
. . . . . . . 8
|
16 | 13, 15 | syl 17 |
. . . . . . 7
|
17 | 16 | adantr 481 |
. . . . . 6
|
18 | 17 | 3ad2ant2 1083 |
. . . . 5
finSupp Scalar
|
19 | 18 | imp 445 |
. . . 4
finSupp Scalar
|
20 | | elelpwi 4171 |
. . . . . . . 8
|
21 | 20 | expcom 451 |
. . . . . . 7
|
22 | 21 | adantl 482 |
. . . . . 6
|
23 | 22 | 3ad2ant1 1082 |
. . . . 5
finSupp Scalar
|
24 | 23 | imp 445 |
. . . 4
finSupp Scalar
|
25 | | eqid 2622 |
. . . . 5
|
26 | 1, 2, 25, 3 | lmodvscl 18880 |
. . . 4
|
27 | 12, 19, 24, 26 | syl3anc 1326 |
. . 3
finSupp Scalar
|
28 | 2, 3 | scmfsupp 42159 |
. . . 4
finSupp
Scalar finSupp |
29 | 28 | 3adant2r 1321 |
. . 3
finSupp Scalar finSupp |
30 | 1, 2, 3, 4, 5, 6, 7, 9, 11, 27, 29 | gsumvsmul 18927 |
. 2
finSupp Scalar g g |
31 | 2 | lmodring 18871 |
. . . . . . . . . 10
Scalar |
32 | 31 | adantr 481 |
. . . . . . . . 9
Scalar |
33 | 32 | 3ad2ant1 1082 |
. . . . . . . 8
finSupp Scalar Scalar |
34 | 33 | adantr 481 |
. . . . . . 7
finSupp Scalar
Scalar |
35 | 3 | eleq2i 2693 |
. . . . . . . . . . 11
Scalar |
36 | 35 | biimpi 206 |
. . . . . . . . . 10
Scalar |
37 | 36 | adantl 482 |
. . . . . . . . 9
Scalar |
38 | 37 | 3ad2ant2 1083 |
. . . . . . . 8
finSupp Scalar Scalar |
39 | 38 | adantr 481 |
. . . . . . 7
finSupp Scalar
Scalar |
40 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
|
41 | 40, 3 | syl6eleq 2711 |
. . . . . . . . . . . 12
Scalar |
42 | 41 | ex 450 |
. . . . . . . . . . 11
Scalar |
43 | 13, 42 | syl 17 |
. . . . . . . . . 10
Scalar |
44 | 43 | adantr 481 |
. . . . . . . . 9
Scalar |
45 | 44 | 3ad2ant2 1083 |
. . . . . . . 8
finSupp Scalar
Scalar |
46 | 45 | imp 445 |
. . . . . . 7
finSupp Scalar
Scalar |
47 | | eqid 2622 |
. . . . . . . 8
Scalar Scalar |
48 | | lincscm.t |
. . . . . . . 8
Scalar |
49 | 47, 48 | ringcl 18561 |
. . . . . . 7
Scalar
Scalar Scalar Scalar |
50 | 34, 39, 46, 49 | syl3anc 1326 |
. . . . . 6
finSupp Scalar
Scalar |
51 | | lincscm.f |
. . . . . 6
|
52 | 50, 51 | fmptd 6385 |
. . . . 5
finSupp Scalar Scalar |
53 | | fvex 6201 |
. . . . . 6
Scalar |
54 | | elmapg 7870 |
. . . . . 6
Scalar
Scalar Scalar |
55 | 53, 9, 54 | sylancr 695 |
. . . . 5
finSupp Scalar Scalar
Scalar |
56 | 52, 55 | mpbird 247 |
. . . 4
finSupp Scalar Scalar |
57 | | lincval 42198 |
. . . 4
Scalar linC
g |
58 | 7, 56, 9, 57 | syl3anc 1326 |
. . 3
finSupp Scalar linC g |
59 | | simpr 477 |
. . . . . . . 8
finSupp Scalar
|
60 | | ovex 6678 |
. . . . . . . 8
|
61 | | fveq2 6191 |
. . . . . . . . . 10
|
62 | 61 | oveq2d 6666 |
. . . . . . . . 9
|
63 | 62, 51 | fvmptg 6280 |
. . . . . . . 8
|
64 | 59, 60, 63 | sylancl 694 |
. . . . . . 7
finSupp Scalar
|
65 | 64 | oveq1d 6665 |
. . . . . 6
finSupp Scalar
|
66 | 11 | adantr 481 |
. . . . . . . 8
finSupp Scalar
|
67 | 1, 2, 25, 3, 48 | lmodvsass 18888 |
. . . . . . . 8
|
68 | 12, 66, 19, 24, 67 | syl13anc 1328 |
. . . . . . 7
finSupp Scalar
|
69 | 6 | eqcomi 2631 |
. . . . . . . . 9
|
70 | 69 | a1i 11 |
. . . . . . . 8
finSupp Scalar
|
71 | 70 | oveqd 6667 |
. . . . . . 7
finSupp Scalar
|
72 | 68, 71 | eqtrd 2656 |
. . . . . 6
finSupp Scalar
|
73 | 65, 72 | eqtrd 2656 |
. . . . 5
finSupp Scalar
|
74 | 73 | mpteq2dva 4744 |
. . . 4
finSupp Scalar |
75 | 74 | oveq2d 6666 |
. . 3
finSupp Scalar g g |
76 | 58, 75 | eqtrd 2656 |
. 2
finSupp Scalar linC g |
77 | | lincscm.x |
. . . . 5
linC |
78 | 77 | a1i 11 |
. . . 4
finSupp Scalar linC |
79 | 3 | oveq1i 6660 |
. . . . . . . . 9
Scalar |
80 | 79 | eleq2i 2693 |
. . . . . . . 8
Scalar |
81 | 80 | biimpi 206 |
. . . . . . 7
Scalar |
82 | 81 | adantr 481 |
. . . . . 6
Scalar |
83 | 82 | 3ad2ant2 1083 |
. . . . 5
finSupp Scalar Scalar |
84 | | lincval 42198 |
. . . . 5
Scalar linC
g |
85 | 7, 83, 9, 84 | syl3anc 1326 |
. . . 4
finSupp Scalar linC g |
86 | 78, 85 | eqtrd 2656 |
. . 3
finSupp Scalar g |
87 | 86 | oveq2d 6666 |
. 2
finSupp Scalar
g |
88 | 30, 76, 87 | 3eqtr4rd 2667 |
1
finSupp Scalar linC |