Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
|
2 | | eqid 2622 |
. . . . 5
Scalar Scalar |
3 | | eqid 2622 |
. . . . 5
Scalar Scalar |
4 | 1, 2, 3 | lcoval 42201 |
. . . 4
LinCo
Scalar finSupp Scalar
linC |
5 | 1, 2, 3 | lcoval 42201 |
. . . 4
LinCo
Scalar finSupp Scalar
linC |
6 | 4, 5 | anbi12d 747 |
. . 3
LinCo
LinCo
Scalar finSupp Scalar linC
Scalar finSupp Scalar linC |
7 | | simpll 790 |
. . . . . 6
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
8 | | simpll 790 |
. . . . . . 7
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC
|
9 | 8 | adantl 482 |
. . . . . 6
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
10 | | simprl 794 |
. . . . . . 7
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC
|
11 | 10 | adantl 482 |
. . . . . 6
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
12 | | lincsumcl.b |
. . . . . . 7
|
13 | 1, 12 | lmodvacl 18877 |
. . . . . 6
|
14 | 7, 9, 11, 13 | syl3anc 1326 |
. . . . 5
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
15 | 2 | lmodfgrp 18872 |
. . . . . . . . . . . . . . . . . . 19
Scalar |
16 | | grpmnd 17429 |
. . . . . . . . . . . . . . . . . . 19
Scalar Scalar |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Scalar |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Scalar |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar |
20 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
|
22 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
Scalar finSupp Scalar
linC
Scalar |
23 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
Scalar
finSupp Scalar
linC Scalar |
24 | 22, 23 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
Scalar finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar Scalar |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar Scalar |
26 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
Scalar Scalar |
27 | 3, 26 | ofaddmndmap 42122 |
. . . . . . . . . . . . . . . 16
Scalar
Scalar Scalar Scalar Scalar |
28 | 19, 21, 25, 27 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar Scalar |
29 | 17 | anim1i 592 |
. . . . . . . . . . . . . . . . 17
Scalar |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar
|
31 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
Scalar
finSupp Scalar
linC finSupp
Scalar |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Scalar finSupp Scalar
linC
finSupp Scalar |
33 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
Scalar
finSupp Scalar
linC finSupp
Scalar |
34 | 32, 33 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
Scalar finSupp Scalar
linC
Scalar
finSupp Scalar
linC
finSupp Scalar finSupp Scalar |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
finSupp
Scalar
finSupp Scalar |
36 | 3 | mndpfsupp 42157 |
. . . . . . . . . . . . . . . 16
Scalar
Scalar Scalar
finSupp Scalar finSupp
Scalar Scalar finSupp Scalar |
37 | 30, 25, 35, 36 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar finSupp Scalar |
38 | | oveq12 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
linC linC
linC linC |
39 | 38 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
linC linC linC linC |
40 | 39 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
finSupp Scalar linC linC linC linC |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
Scalar
finSupp Scalar
linC linC linC linC |
42 | 41 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
linC Scalar
finSupp Scalar
linC linC linC |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
finSupp Scalar linC Scalar
finSupp Scalar
linC linC linC |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Scalar
finSupp Scalar
linC Scalar
finSupp Scalar
linC linC linC |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC linC linC |
46 | 45 | imp 445 |
. . . . . . . . . . . . . . . . 17
Scalar finSupp Scalar
linC
Scalar
finSupp Scalar
linC
linC linC |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
linC linC |
48 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
|
49 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
linC linC |
50 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
linC linC |
51 | 12, 49, 50, 2, 3, 26 | lincsum 42218 |
. . . . . . . . . . . . . . . . 17
Scalar Scalar
finSupp Scalar finSupp
Scalar linC linC Scalar linC |
52 | 48, 25, 35, 51 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
linC linC Scalar linC |
53 | 47, 52 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar linC |
54 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
Scalar
finSupp Scalar
Scalar finSupp Scalar |
55 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
Scalar
linC Scalar linC |
56 | 55 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
Scalar
linC Scalar linC |
57 | 54, 56 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
Scalar
finSupp Scalar
linC Scalar finSupp Scalar Scalar linC |
58 | 57 | rspcev 3309 |
. . . . . . . . . . . . . . 15
Scalar Scalar
Scalar finSupp Scalar Scalar linC
Scalar finSupp Scalar
linC |
59 | 28, 37, 53, 58 | syl12anc 1324 |
. . . . . . . . . . . . . 14
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar finSupp Scalar linC |
60 | 59 | exp41 638 |
. . . . . . . . . . . . 13
Scalar
finSupp Scalar
linC
Scalar
finSupp Scalar
linC
Scalar finSupp Scalar
linC |
61 | 60 | rexlimiva 3028 |
. . . . . . . . . . . 12
Scalar finSupp Scalar linC
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
62 | 61 | expd 452 |
. . . . . . . . . . 11
Scalar finSupp Scalar linC
Scalar
finSupp Scalar
linC
Scalar finSupp Scalar
linC |
63 | 62 | impcom 446 |
. . . . . . . . . 10
Scalar finSupp Scalar linC
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
64 | 63 | com13 88 |
. . . . . . . . 9
Scalar
finSupp Scalar
linC
Scalar finSupp Scalar linC Scalar finSupp Scalar
linC |
65 | 64 | rexlimiva 3028 |
. . . . . . . 8
Scalar finSupp Scalar linC
Scalar finSupp Scalar linC Scalar finSupp Scalar
linC |
66 | 65 | impcom 446 |
. . . . . . 7
Scalar finSupp Scalar linC Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
67 | 66 | impcom 446 |
. . . . . 6
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC |
68 | 67 | impcom 446 |
. . . . 5
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC Scalar finSupp Scalar
linC |
69 | 1, 2, 3 | lcoval 42201 |
. . . . . 6
LinCo
Scalar finSupp Scalar
linC |
70 | 69 | adantr 481 |
. . . . 5
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC LinCo
Scalar finSupp Scalar
linC |
71 | 14, 68, 70 | mpbir2and 957 |
. . . 4
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC LinCo |
72 | 71 | ex 450 |
. . 3
Scalar finSupp Scalar
linC
Scalar finSupp Scalar
linC
LinCo |
73 | 6, 72 | sylbid 230 |
. 2
LinCo
LinCo LinCo |
74 | 73 | imp 445 |
1
LinCo LinCo
LinCo |