Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β π β LMod) |
2 | | lincdifsn.s |
. . . . . . . . 9
β’ π = (Baseβπ
) |
3 | | lincdifsn.r |
. . . . . . . . . 10
β’ π
= (Scalarβπ) |
4 | 3 | fveq2i 6850 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
5 | 2, 4 | eqtri 2765 |
. . . . . . . 8
β’ π =
(Baseβ(Scalarβπ)) |
6 | 5 | oveq1i 7372 |
. . . . . . 7
β’ (π βm π) =
((Baseβ(Scalarβπ)) βm π) |
7 | 6 | eleq2i 2830 |
. . . . . 6
β’ (πΉ β (π βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
8 | 7 | biimpi 215 |
. . . . 5
β’ (πΉ β (π βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
9 | 8 | adantr 482 |
. . . 4
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
10 | 9 | 3ad2ant2 1135 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
11 | | lincdifsn.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
12 | 11 | pweqi 4581 |
. . . . . . 7
β’ π«
π΅ = π«
(Baseβπ) |
13 | 12 | eleq2i 2830 |
. . . . . 6
β’ (π β π« π΅ β π β π« (Baseβπ)) |
14 | 13 | biimpi 215 |
. . . . 5
β’ (π β π« π΅ β π β π« (Baseβπ)) |
15 | 14 | 3ad2ant2 1135 |
. . . 4
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β π β π« (Baseβπ)) |
16 | 15 | 3ad2ant1 1134 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β π β π« (Baseβπ)) |
17 | | lincval 46564 |
. . 3
β’ ((π β LMod β§ πΉ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (πΉ( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯)))) |
18 | 1, 10, 16, 17 | syl3anc 1372 |
. 2
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΉ( linC βπ)π) = (π Ξ£g (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯)))) |
19 | | lincdifsn.p |
. . . 4
β’ + =
(+gβπ) |
20 | | lmodcmn 20386 |
. . . . . 6
β’ (π β LMod β π β CMnd) |
21 | 20 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β π β CMnd) |
22 | 21 | 3ad2ant1 1134 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β π β CMnd) |
23 | | simp12 1205 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β π β π« π΅) |
24 | 14 | anim2i 618 |
. . . . . . 7
β’ ((π β LMod β§ π β π« π΅) β (π β LMod β§ π β π« (Baseβπ))) |
25 | 24 | 3adant3 1133 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (π β LMod β§ π β π« (Baseβπ))) |
26 | 25 | 3ad2ant1 1134 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π β LMod β§ π β π« (Baseβπ))) |
27 | | simp2l 1200 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΉ β (π βm π)) |
28 | | lincdifsn.0 |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
29 | 28 | breq2i 5118 |
. . . . . . . 8
β’ (πΉ finSupp 0 β πΉ finSupp (0gβπ
)) |
30 | 29 | biimpi 215 |
. . . . . . 7
β’ (πΉ finSupp 0 β πΉ finSupp (0gβπ
)) |
31 | 30 | adantl 483 |
. . . . . 6
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ finSupp (0gβπ
)) |
32 | 31 | 3ad2ant2 1135 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΉ finSupp (0gβπ
)) |
33 | 3, 2 | scmfsupp 46528 |
. . . . 5
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΉ β (π βm π) β§ πΉ finSupp (0gβπ
)) β (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
34 | 26, 27, 32, 33 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯)) finSupp (0gβπ)) |
35 | | simpl1 1192 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β LMod) |
36 | 35 | adantr 482 |
. . . . . 6
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π₯ β π) β π β LMod) |
37 | | elmapi 8794 |
. . . . . . . . . 10
β’ (πΉ β (π βm π) β πΉ:πβΆπ) |
38 | | ffvelcdm 7037 |
. . . . . . . . . . . 12
β’ ((πΉ:πβΆπ β§ π₯ β π) β (πΉβπ₯) β π) |
39 | 38 | ex 414 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β (π₯ β π β (πΉβπ₯) β π)) |
40 | 39 | a1d 25 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β ((π β LMod β§ π β π« π΅ β§ π β π) β (π₯ β π β (πΉβπ₯) β π))) |
41 | 37, 40 | syl 17 |
. . . . . . . . 9
β’ (πΉ β (π βm π) β ((π β LMod β§ π β π« π΅ β§ π β π) β (π₯ β π β (πΉβπ₯) β π))) |
42 | 41 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β ((π β LMod β§ π β π« π΅ β§ π β π) β (π₯ β π β (πΉβπ₯) β π))) |
43 | 42 | impcom 409 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π₯ β π β (πΉβπ₯) β π)) |
44 | 43 | imp 408 |
. . . . . 6
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π₯ β π) β (πΉβπ₯) β π) |
45 | | elelpwi 4575 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π β π« π΅) β π₯ β π΅) |
46 | 45 | expcom 415 |
. . . . . . . . 9
β’ (π β π« π΅ β (π₯ β π β π₯ β π΅)) |
47 | 46 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (π₯ β π β π₯ β π΅)) |
48 | 47 | adantr 482 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π₯ β π β π₯ β π΅)) |
49 | 48 | imp 408 |
. . . . . 6
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π₯ β π) β π₯ β π΅) |
50 | | eqid 2737 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
51 | 11, 3, 50, 2 | lmodvscl 20355 |
. . . . . 6
β’ ((π β LMod β§ (πΉβπ₯) β π β§ π₯ β π΅) β ((πΉβπ₯)( Β·π
βπ)π₯) β π΅) |
52 | 36, 44, 49, 51 | syl3anc 1372 |
. . . . 5
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π₯ β π) β ((πΉβπ₯)( Β·π
βπ)π₯) β π΅) |
53 | 52 | 3adantl3 1169 |
. . . 4
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β§ π₯ β π) β ((πΉβπ₯)( Β·π
βπ)π₯) β π΅) |
54 | | simp13 1206 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β π β π) |
55 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆπ β§ π β π) β (πΉβπ) β π) |
56 | 55 | expcom 415 |
. . . . . . . . . 10
β’ (π β π β (πΉ:πβΆπ β (πΉβπ) β π)) |
57 | 56 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉ:πβΆπ β (πΉβπ) β π)) |
58 | 37, 57 | syl5com 31 |
. . . . . . . 8
β’ (πΉ β (π βm π) β ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉβπ) β π)) |
59 | 58 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β ((π β LMod β§ π β π« π΅ β§ π β π) β (πΉβπ) β π)) |
60 | 59 | impcom 409 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉβπ) β π) |
61 | | elelpwi 4575 |
. . . . . . . . 9
β’ ((π β π β§ π β π« π΅) β π β π΅) |
62 | 61 | ancoms 460 |
. . . . . . . 8
β’ ((π β π« π΅ β§ π β π) β π β π΅) |
63 | 62 | 3adant1 1131 |
. . . . . . 7
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β π β π΅) |
64 | 63 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β π΅) |
65 | | lincdifsn.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
66 | 11, 3, 65, 2 | lmodvscl 20355 |
. . . . . 6
β’ ((π β LMod β§ (πΉβπ) β π β§ π β π΅) β ((πΉβπ) Β· π) β π΅) |
67 | 35, 60, 64, 66 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β ((πΉβπ) Β· π) β π΅) |
68 | 67 | 3adant3 1133 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β ((πΉβπ) Β· π) β π΅) |
69 | 65 | eqcomi 2746 |
. . . . . . 7
β’ (
Β·π βπ) = Β· |
70 | 69 | a1i 11 |
. . . . . 6
β’ (π₯ = π β (
Β·π βπ) = Β· ) |
71 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
72 | | id 22 |
. . . . . 6
β’ (π₯ = π β π₯ = π) |
73 | 70, 71, 72 | oveq123d 7383 |
. . . . 5
β’ (π₯ = π β ((πΉβπ₯)( Β·π
βπ)π₯) = ((πΉβπ) Β· π)) |
74 | 73 | adantl 483 |
. . . 4
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β§ π₯ = π) β ((πΉβπ₯)( Β·π
βπ)π₯) = ((πΉβπ) Β· π)) |
75 | 11, 19, 22, 23, 34, 53, 54, 68, 74 | gsumdifsnd 19745 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π Ξ£g (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) = ((π Ξ£g (π₯ β (π β {π}) β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) + ((πΉβπ) Β· π))) |
76 | | fveq1 6846 |
. . . . . . . . . 10
β’ (πΊ = (πΉ βΎ (π β {π})) β (πΊβπ₯) = ((πΉ βΎ (π β {π}))βπ₯)) |
77 | 76 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΊβπ₯) = ((πΉ βΎ (π β {π}))βπ₯)) |
78 | | fvres 6866 |
. . . . . . . . 9
β’ (π₯ β (π β {π}) β ((πΉ βΎ (π β {π}))βπ₯) = (πΉβπ₯)) |
79 | 77, 78 | sylan9eq 2797 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β§ π₯ β (π β {π})) β (πΊβπ₯) = (πΉβπ₯)) |
80 | 79 | oveq1d 7377 |
. . . . . . 7
β’ ((((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β§ π₯ β (π β {π})) β ((πΊβπ₯)( Β·π
βπ)π₯) = ((πΉβπ₯)( Β·π
βπ)π₯)) |
81 | 80 | mpteq2dva 5210 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯)) = (π₯ β (π β {π}) β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) |
82 | 81 | eqcomd 2743 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π₯ β (π β {π}) β¦ ((πΉβπ₯)( Β·π
βπ)π₯)) = (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯))) |
83 | 82 | oveq2d 7378 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π Ξ£g (π₯ β (π β {π}) β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) = (π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯)))) |
84 | 83 | oveq1d 7377 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β ((π Ξ£g (π₯ β (π β {π}) β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) + ((πΉβπ) Β· π)) = ((π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯))) + ((πΉβπ) Β· π))) |
85 | 75, 84 | eqtrd 2777 |
. 2
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π Ξ£g (π₯ β π β¦ ((πΉβπ₯)( Β·π
βπ)π₯))) = ((π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯))) + ((πΉβπ) Β· π))) |
86 | | eqid 2737 |
. . . . . . . . . . . 12
β’ π = π |
87 | 86, 5 | feq23i 6667 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β πΉ:πβΆ(Baseβ(Scalarβπ))) |
88 | 37, 87 | sylib 217 |
. . . . . . . . . 10
β’ (πΉ β (π βm π) β πΉ:πβΆ(Baseβ(Scalarβπ))) |
89 | 88 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ:πβΆ(Baseβ(Scalarβπ))) |
90 | 89 | 3ad2ant2 1135 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΉ:πβΆ(Baseβ(Scalarβπ))) |
91 | | difssd 4097 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π β {π}) β π) |
92 | 90, 91 | fssresd 6714 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΉ βΎ (π β {π})):(π β {π})βΆ(Baseβ(Scalarβπ))) |
93 | | feq1 6654 |
. . . . . . . 8
β’ (πΊ = (πΉ βΎ (π β {π})) β (πΊ:(π β {π})βΆ(Baseβ(Scalarβπ)) β (πΉ βΎ (π β {π})):(π β {π})βΆ(Baseβ(Scalarβπ)))) |
94 | 93 | 3ad2ant3 1136 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΊ:(π β {π})βΆ(Baseβ(Scalarβπ)) β (πΉ βΎ (π β {π})):(π β {π})βΆ(Baseβ(Scalarβπ)))) |
95 | 92, 94 | mpbird 257 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΊ:(π β {π})βΆ(Baseβ(Scalarβπ))) |
96 | | fvex 6860 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) β V |
97 | | difexg 5289 |
. . . . . . . . 9
β’ (π β π« π΅ β (π β {π}) β V) |
98 | 97 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (π β {π}) β V) |
99 | 98 | 3ad2ant1 1134 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π β {π}) β V) |
100 | | elmapg 8785 |
. . . . . . 7
β’
(((Baseβ(Scalarβπ)) β V β§ (π β {π}) β V) β (πΊ β ((Baseβ(Scalarβπ)) βm (π β {π})) β πΊ:(π β {π})βΆ(Baseβ(Scalarβπ)))) |
101 | 96, 99, 100 | sylancr 588 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΊ β ((Baseβ(Scalarβπ)) βm (π β {π})) β πΊ:(π β {π})βΆ(Baseβ(Scalarβπ)))) |
102 | 95, 101 | mpbird 257 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β πΊ β ((Baseβ(Scalarβπ)) βm (π β {π}))) |
103 | | elpwi 4572 |
. . . . . . . . . 10
β’ (π β π« π΅ β π β π΅) |
104 | 11 | sseq2i 3978 |
. . . . . . . . . . . 12
β’ (π β π΅ β π β (Baseβπ)) |
105 | 104 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β π΅ β π β (Baseβπ)) |
106 | 105 | ssdifssd 4107 |
. . . . . . . . . 10
β’ (π β π΅ β (π β {π}) β (Baseβπ)) |
107 | 103, 106 | syl 17 |
. . . . . . . . 9
β’ (π β π« π΅ β (π β {π}) β (Baseβπ)) |
108 | 107 | adantl 483 |
. . . . . . . 8
β’ ((π β LMod β§ π β π« π΅) β (π β {π}) β (Baseβπ)) |
109 | 97 | adantl 483 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π« π΅) β (π β {π}) β V) |
110 | | elpwg 4568 |
. . . . . . . . 9
β’ ((π β {π}) β V β ((π β {π}) β π« (Baseβπ) β (π β {π}) β (Baseβπ))) |
111 | 109, 110 | syl 17 |
. . . . . . . 8
β’ ((π β LMod β§ π β π« π΅) β ((π β {π}) β π« (Baseβπ) β (π β {π}) β (Baseβπ))) |
112 | 108, 111 | mpbird 257 |
. . . . . . 7
β’ ((π β LMod β§ π β π« π΅) β (π β {π}) β π« (Baseβπ)) |
113 | 112 | 3adant3 1133 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅ β§ π β π) β (π β {π}) β π« (Baseβπ)) |
114 | 113 | 3ad2ant1 1134 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π β {π}) β π« (Baseβπ)) |
115 | | lincval 46564 |
. . . . 5
β’ ((π β LMod β§ πΊ β
((Baseβ(Scalarβπ)) βm (π β {π})) β§ (π β {π}) β π« (Baseβπ)) β (πΊ( linC βπ)(π β {π})) = (π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯)))) |
116 | 1, 102, 114, 115 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΊ( linC βπ)(π β {π})) = (π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯)))) |
117 | 116 | eqcomd 2743 |
. . 3
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯))) = (πΊ( linC βπ)(π β {π}))) |
118 | 117 | oveq1d 7377 |
. 2
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β ((π Ξ£g (π₯ β (π β {π}) β¦ ((πΊβπ₯)( Β·π
βπ)π₯))) + ((πΉβπ) Β· π)) = ((πΊ( linC βπ)(π β {π})) + ((πΉβπ) Β· π))) |
119 | 18, 85, 118 | 3eqtrd 2781 |
1
β’ (((π β LMod β§ π β π« π΅ β§ π β π) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 ) β§ πΊ = (πΉ βΎ (π β {π}))) β (πΉ( linC βπ)π) = ((πΊ( linC βπ)(π β {π})) + ((πΉβπ) Β· π))) |