Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | lincscmcl.r |
. . . . 5
β’ π
=
(Baseβ(Scalarβπ)) |
4 | 1, 2, 3 | lcoval 46583 |
. . . 4
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
(π· β (π LinCo π) β (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) |
5 | 4 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β (π· β (π LinCo π) β (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))))) |
6 | | simpl 484 |
. . . . . . 7
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β
LMod) |
7 | 6 | ad2antrr 725 |
. . . . . 6
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β π β LMod) |
8 | | simpr 486 |
. . . . . . 7
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β πΆ β π
) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β πΆ β π
) |
10 | | simprl 770 |
. . . . . 6
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β π· β (Baseβπ)) |
11 | | lincscmcl.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
12 | 1, 2, 11, 3 | lmodvscl 20383 |
. . . . . 6
β’ ((π β LMod β§ πΆ β π
β§ π· β (Baseβπ)) β (πΆ Β· π·) β (Baseβπ)) |
13 | 7, 9, 10, 12 | syl3anc 1372 |
. . . . 5
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (πΆ Β· π·) β (Baseβπ)) |
14 | 2 | lmodring 20373 |
. . . . . . . . . . . . . . . . 17
β’ (π β LMod β
(Scalarβπ) β
Ring) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β (Scalarβπ) β Ring) |
16 | 15 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (Scalarβπ) β Ring) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β§ π£ β π) β (Scalarβπ) β Ring) |
18 | 8 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β πΆ β π
) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β§ π£ β π) β πΆ β π
) |
20 | | elmapi 8793 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π
βm π) β π₯:πβΆπ
) |
21 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯:πβΆπ
β§ π£ β π) β (π₯βπ£) β π
) |
22 | 21 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯:πβΆπ
β (π£ β π β (π₯βπ£) β π
)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π
βm π) β (π£ β π β (π₯βπ£) β π
)) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (π£ β π β (π₯βπ£) β π
)) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π£ β π β (π₯βπ£) β π
)) |
26 | 25 | imp 408 |
. . . . . . . . . . . . . 14
β’
(((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β§ π£ β π) β (π₯βπ£) β π
) |
27 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
28 | 3, 27 | ringcl 19989 |
. . . . . . . . . . . . . 14
β’
(((Scalarβπ)
β Ring β§ πΆ β
π
β§ (π₯βπ£) β π
) β (πΆ(.rβ(Scalarβπ))(π₯βπ£)) β π
) |
29 | 17, 19, 26, 28 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
(((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β§ π£ β π) β (πΆ(.rβ(Scalarβπ))(π₯βπ£)) β π
) |
30 | 29 | fmpttd 7067 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))):πβΆπ
) |
31 | 3 | fvexi 6860 |
. . . . . . . . . . . . 13
β’ π
β V |
32 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
π β π«
(Baseβπ)) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β π β π« (Baseβπ)) |
34 | 33 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β π β π« (Baseβπ)) |
35 | | elmapg 8784 |
. . . . . . . . . . . . 13
β’ ((π
β V β§ π β π«
(Baseβπ)) β
((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π
βm π) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))):πβΆπ
)) |
36 | 31, 34, 35 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π
βm π) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))):πβΆπ
)) |
37 | 30, 36 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π
βm π)) |
38 | 15, 33, 8 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β ((Scalarβπ) β Ring β§ π β π« (Baseβπ) β§ πΆ β π
)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β ((Scalarβπ) β Ring β§ π β π« (Baseβπ) β§ πΆ β π
)) |
40 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β π₯ β (π
βm π)) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β π₯ β (π
βm π)) |
42 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β π₯ finSupp
(0gβ(Scalarβπ))) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β π₯ finSupp
(0gβ(Scalarβπ))) |
44 | 3 | rmfsupp 46540 |
. . . . . . . . . . . 12
β’
((((Scalarβπ)
β Ring β§ π β
π« (Baseβπ)
β§ πΆ β π
) β§ π₯ β (π
βm π) β§ π₯ finSupp
(0gβ(Scalarβπ))) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) finSupp
(0gβ(Scalarβπ))) |
45 | 39, 41, 43, 44 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) finSupp
(0gβ(Scalarβπ))) |
46 | | oveq2 7369 |
. . . . . . . . . . . . . . 15
β’ (π· = (π₯( linC βπ)π) β (πΆ Β· π·) = (πΆ Β· (π₯( linC βπ)π))) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)) β (πΆ Β· π·) = (πΆ Β· (π₯( linC βπ)π))) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ Β· π·) = (πΆ Β· (π₯( linC βπ)π))) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (πΆ Β· π·) = (πΆ Β· (π₯( linC βπ)π))) |
50 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π β LMod β§ π β π« (Baseβπ))) |
51 | 40 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β π₯ β (π
βm π)) |
52 | 51, 8 | anim12i 614 |
. . . . . . . . . . . . 13
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (π₯ β (π
βm π) β§ πΆ β π
)) |
53 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯( linC βπ)π) = (π₯( linC βπ)π) |
54 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) = (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) |
55 | 11, 27, 53, 3, 54 | lincscm 46601 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π₯ β (π
βm π) β§ πΆ β π
) β§ π₯ finSupp
(0gβ(Scalarβπ))) β (πΆ Β· (π₯( linC βπ)π)) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π)) |
56 | 50, 52, 43, 55 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (πΆ Β· (π₯( linC βπ)π)) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π)) |
57 | 49, 56 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β (πΆ Β· π·) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π)) |
58 | | breq1 5112 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π finSupp
(0gβ(Scalarβπ)) β (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) finSupp
(0gβ(Scalarβπ)))) |
59 | | oveq1 7368 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π ( linC βπ)π) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π)) |
60 | 59 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β ((πΆ Β· π·) = (π ( linC βπ)π) β (πΆ Β· π·) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π))) |
61 | 58, 60 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = (π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β ((π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π)) β ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π)))) |
62 | 61 | rspcev 3583 |
. . . . . . . . . . 11
β’ (((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) β (π
βm π) β§ ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£))) finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = ((π£ β π β¦ (πΆ(.rβ(Scalarβπ))(π₯βπ£)))( linC βπ)π))) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))) |
63 | 37, 45, 57, 62 | syl12anc 836 |
. . . . . . . . . 10
β’ ((((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β§ ((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
)) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))) |
64 | 63 | ex 414 |
. . . . . . . . 9
β’ (((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β§ π· β (Baseβπ)) β (((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π)))) |
65 | 64 | ex 414 |
. . . . . . . 8
β’ ((π₯ β (π
βm π) β§ (π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (π· β (Baseβπ) β (((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))))) |
66 | 65 | rexlimiva 3141 |
. . . . . . 7
β’
(βπ₯ β
(π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)) β (π· β (Baseβπ) β (((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))))) |
67 | 66 | impcom 409 |
. . . . . 6
β’ ((π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (((π β LMod β§ π β π« (Baseβπ)) β§ πΆ β π
) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π)))) |
68 | 67 | impcom 409 |
. . . . 5
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))) |
69 | 1, 2, 3 | lcoval 46583 |
. . . . . 6
β’ ((π β LMod β§ π β π«
(Baseβπ)) β
((πΆ Β· π·) β (π LinCo π) β ((πΆ Β· π·) β (Baseβπ) β§ βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))))) |
70 | 69 | ad2antrr 725 |
. . . . 5
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β ((πΆ Β· π·) β (π LinCo π) β ((πΆ Β· π·) β (Baseβπ) β§ βπ β (π
βm π)(π finSupp
(0gβ(Scalarβπ)) β§ (πΆ Β· π·) = (π ( linC βπ)π))))) |
71 | 13, 68, 70 | mpbir2and 712 |
. . . 4
β’ ((((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β§ (π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π)))) β (πΆ Β· π·) β (π LinCo π)) |
72 | 71 | ex 414 |
. . 3
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β ((π· β (Baseβπ) β§ βπ₯ β (π
βm π)(π₯ finSupp
(0gβ(Scalarβπ)) β§ π· = (π₯( linC βπ)π))) β (πΆ Β· π·) β (π LinCo π))) |
73 | 5, 72 | sylbid 239 |
. 2
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
) β (π· β (π LinCo π) β (πΆ Β· π·) β (π LinCo π))) |
74 | 73 | 3impia 1118 |
1
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΆ β π
β§ π· β (π LinCo π)) β (πΆ Β· π·) β (π LinCo π)) |