Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β π β LMod) |
2 | | lincvalsc0.s |
. . . . . . . 8
β’ π = (Scalarβπ) |
3 | 2 | eqcomi 2742 |
. . . . . . . . 9
β’
(Scalarβπ) =
π |
4 | 3 | fveq2i 6849 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβπ) |
5 | | lincvalsc0.0 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
6 | 2, 4, 5 | lmod0cl 20392 |
. . . . . . 7
β’ (π β LMod β 0 β
(Baseβ(Scalarβπ))) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π β LMod β§ π β π« π΅) β 0 β
(Baseβ(Scalarβπ))) |
8 | 7 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π₯ β π) β 0 β
(Baseβ(Scalarβπ))) |
9 | | lincvalsc0.f |
. . . . 5
β’ πΉ = (π₯ β π β¦ 0 ) |
10 | 8, 9 | fmptd 7066 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β πΉ:πβΆ(Baseβ(Scalarβπ))) |
11 | | fvexd 6861 |
. . . . 5
β’ (π β LMod β
(Baseβ(Scalarβπ)) β V) |
12 | | elmapg 8784 |
. . . . 5
β’
(((Baseβ(Scalarβπ)) β V β§ π β π« π΅) β (πΉ β ((Baseβ(Scalarβπ)) βm π) β πΉ:πβΆ(Baseβ(Scalarβπ)))) |
13 | 11, 12 | sylan 581 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β (πΉ β ((Baseβ(Scalarβπ)) βm π) β πΉ:πβΆ(Baseβ(Scalarβπ)))) |
14 | 10, 13 | mpbird 257 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
15 | | lincvalsc0.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
16 | 15 | pweqi 4580 |
. . . . . 6
β’ π«
π΅ = π«
(Baseβπ) |
17 | 16 | eleq2i 2826 |
. . . . 5
β’ (π β π« π΅ β π β π« (Baseβπ)) |
18 | 17 | biimpi 215 |
. . . 4
β’ (π β π« π΅ β π β π« (Baseβπ)) |
19 | 18 | adantl 483 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β π β π« (Baseβπ)) |
20 | | lincval 46580 |
. . 3
β’ ((π β LMod β§ πΉ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
21 | 1, 14, 19, 20 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
22 | | simpr 486 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π£ β π) |
23 | 5 | fvexi 6860 |
. . . . . . 7
β’ 0 β
V |
24 | | eqidd 2734 |
. . . . . . . 8
β’ (π₯ = π£ β 0 = 0 ) |
25 | 24, 9 | fvmptg 6950 |
. . . . . . 7
β’ ((π£ β π β§ 0 β V) β (πΉβπ£) = 0 ) |
26 | 22, 23, 25 | sylancl 587 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β (πΉβπ£) = 0 ) |
27 | 26 | oveq1d 7376 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) = ( 0 (
Β·π βπ)π£)) |
28 | 1 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π β LMod) |
29 | | elelpwi 4574 |
. . . . . . . . 9
β’ ((π£ β π β§ π β π« π΅) β π£ β π΅) |
30 | 29 | expcom 415 |
. . . . . . . 8
β’ (π β π« π΅ β (π£ β π β π£ β π΅)) |
31 | 30 | adantl 483 |
. . . . . . 7
β’ ((π β LMod β§ π β π« π΅) β (π£ β π β π£ β π΅)) |
32 | 31 | imp 408 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π£ β π΅) |
33 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
34 | | lincvalsc0.z |
. . . . . . 7
β’ π = (0gβπ) |
35 | 15, 2, 33, 5, 34 | lmod0vs 20399 |
. . . . . 6
β’ ((π β LMod β§ π£ β π΅) β ( 0 (
Β·π βπ)π£) = π) |
36 | 28, 32, 35 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ( 0 (
Β·π βπ)π£) = π) |
37 | 27, 36 | eqtrd 2773 |
. . . 4
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) = π) |
38 | 37 | mpteq2dva 5209 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) = (π£ β π β¦ π)) |
39 | 38 | oveq2d 7377 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) = (π Ξ£g (π£ β π β¦ π))) |
40 | | lmodgrp 20372 |
. . . 4
β’ (π β LMod β π β Grp) |
41 | 40 | grpmndd 18768 |
. . 3
β’ (π β LMod β π β Mnd) |
42 | 34 | gsumz 18654 |
. . 3
β’ ((π β Mnd β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ π)) = π) |
43 | 41, 42 | sylan 581 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ π)) = π) |
44 | 21, 39, 43 | 3eqtrd 2777 |
1
β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = π) |