Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β π β LMod) |
2 | | linc0scn0.s |
. . . . . . . . 9
β’ π = (Scalarβπ) |
3 | 2 | lmodring 20373 |
. . . . . . . 8
β’ (π β LMod β π β Ring) |
4 | 2 | eqcomi 2742 |
. . . . . . . . . . 11
β’
(Scalarβπ) =
π |
5 | 4 | fveq2i 6849 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβπ)) = (Baseβπ) |
6 | | linc0scn0.1 |
. . . . . . . . . 10
β’ 1 =
(1rβπ) |
7 | 5, 6 | ringidcl 19997 |
. . . . . . . . 9
β’ (π β Ring β 1 β
(Baseβ(Scalarβπ))) |
8 | | linc0scn0.0 |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
9 | 5, 8 | ring0cl 19998 |
. . . . . . . . 9
β’ (π β Ring β 0 β
(Baseβ(Scalarβπ))) |
10 | 7, 9 | jca 513 |
. . . . . . . 8
β’ (π β Ring β ( 1 β
(Baseβ(Scalarβπ)) β§ 0 β
(Baseβ(Scalarβπ)))) |
11 | 3, 10 | syl 17 |
. . . . . . 7
β’ (π β LMod β ( 1 β
(Baseβ(Scalarβπ)) β§ 0 β
(Baseβ(Scalarβπ)))) |
12 | 11 | ad2antrr 725 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ π₯ β π) β ( 1 β
(Baseβ(Scalarβπ)) β§ 0 β
(Baseβ(Scalarβπ)))) |
13 | | ifcl 4535 |
. . . . . 6
β’ (( 1 β
(Baseβ(Scalarβπ)) β§ 0 β
(Baseβ(Scalarβπ))) β if(π₯ = π, 1 , 0 ) β
(Baseβ(Scalarβπ))) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π₯ β π) β if(π₯ = π, 1 , 0 ) β
(Baseβ(Scalarβπ))) |
15 | | linc0scn0.f |
. . . . 5
β’ πΉ = (π₯ β π β¦ if(π₯ = π, 1 , 0 )) |
16 | 14, 15 | fmptd 7066 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β πΉ:πβΆ(Baseβ(Scalarβπ))) |
17 | | fvex 6859 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) β V |
18 | 17 | a1i 11 |
. . . . 5
β’ (π β LMod β
(Baseβ(Scalarβπ)) β V) |
19 | | elmapg 8784 |
. . . . 5
β’
(((Baseβ(Scalarβπ)) β V β§ π β π« π΅) β (πΉ β ((Baseβ(Scalarβπ)) βm π) β πΉ:πβΆ(Baseβ(Scalarβπ)))) |
20 | 18, 19 | sylan 581 |
. . . 4
β’ ((π β LMod β§ π β π« π΅) β (πΉ β ((Baseβ(Scalarβπ)) βm π) β πΉ:πβΆ(Baseβ(Scalarβπ)))) |
21 | 16, 20 | mpbird 257 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
22 | | linc0scn0.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
23 | 22 | pweqi 4580 |
. . . . . 6
β’ π«
π΅ = π«
(Baseβπ) |
24 | 23 | eleq2i 2826 |
. . . . 5
β’ (π β π« π΅ β π β π« (Baseβπ)) |
25 | 24 | biimpi 215 |
. . . 4
β’ (π β π« π΅ β π β π« (Baseβπ)) |
26 | 25 | adantl 483 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β π β π« (Baseβπ)) |
27 | | lincval 46580 |
. . 3
β’ ((π β LMod β§ πΉ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
28 | 1, 21, 26, 27 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
29 | | simpr 486 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π£ β π) |
30 | 6 | fvexi 6860 |
. . . . . . . 8
β’ 1 β
V |
31 | 8 | fvexi 6860 |
. . . . . . . 8
β’ 0 β
V |
32 | 30, 31 | ifex 4540 |
. . . . . . 7
β’ if(π£ = π, 1 , 0 ) β
V |
33 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π₯ = π£ β (π₯ = π β π£ = π)) |
34 | 33 | ifbid 4513 |
. . . . . . . 8
β’ (π₯ = π£ β if(π₯ = π, 1 , 0 ) = if(π£ = π, 1 , 0 )) |
35 | 34, 15 | fvmptg 6950 |
. . . . . . 7
β’ ((π£ β π β§ if(π£ = π, 1 , 0 ) β V) β (πΉβπ£) = if(π£ = π, 1 , 0 )) |
36 | 29, 32, 35 | sylancl 587 |
. . . . . 6
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β (πΉβπ£) = if(π£ = π, 1 , 0 )) |
37 | 36 | oveq1d 7376 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) = (if(π£ = π, 1 , 0 )(
Β·π βπ)π£)) |
38 | | ovif 7458 |
. . . . . 6
β’ (if(π£ = π, 1 , 0 )(
Β·π βπ)π£) = if(π£ = π, ( 1 (
Β·π βπ)π£), ( 0 (
Β·π βπ)π£)) |
39 | 38 | a1i 11 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β (if(π£ = π, 1 , 0 )(
Β·π βπ)π£) = if(π£ = π, ( 1 (
Β·π βπ)π£), ( 0 (
Β·π βπ)π£))) |
40 | | oveq2 7369 |
. . . . . . . 8
β’ (π£ = π β ( 1 (
Β·π βπ)π£) = ( 1 (
Β·π βπ)π)) |
41 | 40 | adantl 483 |
. . . . . . 7
β’ ((((π β LMod β§ π β π« π΅) β§ π£ β π) β§ π£ = π) β ( 1 (
Β·π βπ)π£) = ( 1 (
Β·π βπ)π)) |
42 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
43 | 2, 42, 6 | lmod1cl 20393 |
. . . . . . . . . . 11
β’ (π β LMod β 1 β
(Baseβπ)) |
44 | 43 | ancli 550 |
. . . . . . . . . 10
β’ (π β LMod β (π β LMod β§ 1 β
(Baseβπ))) |
45 | 44 | adantr 482 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π« π΅) β (π β LMod β§ 1 β (Baseβπ))) |
46 | 45 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π« π΅) β§ π£ β π) β§ π£ = π) β (π β LMod β§ 1 β (Baseβπ))) |
47 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
48 | | linc0scn0.z |
. . . . . . . . 9
β’ π = (0gβπ) |
49 | 2, 47, 42, 48 | lmodvs0 20400 |
. . . . . . . 8
β’ ((π β LMod β§ 1 β
(Baseβπ)) β (
1 (
Β·π βπ)π) = π) |
50 | 46, 49 | syl 17 |
. . . . . . 7
β’ ((((π β LMod β§ π β π« π΅) β§ π£ β π) β§ π£ = π) β ( 1 (
Β·π βπ)π) = π) |
51 | 41, 50 | eqtrd 2773 |
. . . . . 6
β’ ((((π β LMod β§ π β π« π΅) β§ π£ β π) β§ π£ = π) β ( 1 (
Β·π βπ)π£) = π) |
52 | 1 | adantr 482 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π β LMod) |
53 | | elelpwi 4574 |
. . . . . . . . . . 11
β’ ((π£ β π β§ π β π« π΅) β π£ β π΅) |
54 | 53 | expcom 415 |
. . . . . . . . . 10
β’ (π β π« π΅ β (π£ β π β π£ β π΅)) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π« π΅) β (π£ β π β π£ β π΅)) |
56 | 55 | imp 408 |
. . . . . . . 8
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β π£ β π΅) |
57 | 22, 2, 47, 8, 48 | lmod0vs 20399 |
. . . . . . . 8
β’ ((π β LMod β§ π£ β π΅) β ( 0 (
Β·π βπ)π£) = π) |
58 | 52, 56, 57 | syl2anc 585 |
. . . . . . 7
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ( 0 (
Β·π βπ)π£) = π) |
59 | 58 | adantr 482 |
. . . . . 6
β’ ((((π β LMod β§ π β π« π΅) β§ π£ β π) β§ Β¬ π£ = π) β ( 0 (
Β·π βπ)π£) = π) |
60 | 51, 59 | ifeqda 4526 |
. . . . 5
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β if(π£ = π, ( 1 (
Β·π βπ)π£), ( 0 (
Β·π βπ)π£)) = π) |
61 | 37, 39, 60 | 3eqtrd 2777 |
. . . 4
β’ (((π β LMod β§ π β π« π΅) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) = π) |
62 | 61 | mpteq2dva 5209 |
. . 3
β’ ((π β LMod β§ π β π« π΅) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) = (π£ β π β¦ π)) |
63 | 62 | oveq2d 7377 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) = (π Ξ£g (π£ β π β¦ π))) |
64 | | lmodgrp 20372 |
. . . 4
β’ (π β LMod β π β Grp) |
65 | 64 | grpmndd 18768 |
. . 3
β’ (π β LMod β π β Mnd) |
66 | 48 | gsumz 18654 |
. . 3
β’ ((π β Mnd β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ π)) = π) |
67 | 65, 66 | sylan 581 |
. 2
β’ ((π β LMod β§ π β π« π΅) β (π Ξ£g (π£ β π β¦ π)) = π) |
68 | 28, 63, 67 | 3eqtrd 2777 |
1
β’ ((π β LMod β§ π β π« π΅) β (πΉ( linC βπ)π) = π) |