Step | Hyp | Ref
| Expression |
1 | | raldifsni 4756 |
. . . . 5
β’
(βπ β
((Baseβπ
) β
{π}) Β¬
(((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ β (Baseβπ
)((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β π = π)) |
2 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β LMod) |
3 | | simprll 778 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β (Baseβπ
)) |
4 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:πΌβΆπ΅ β§ π β πΌ) β (πΉβπ) β π΅) |
5 | 4 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (πΉβπ) β π΅) |
6 | 5 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (πΉβπ) β π΅) |
7 | | islindf4.b |
. . . . . . . . . . . . . . . . 17
β’ π΅ = (Baseβπ) |
8 | | islindf4.r |
. . . . . . . . . . . . . . . . 17
β’ π
= (Scalarβπ) |
9 | | islindf4.t |
. . . . . . . . . . . . . . . . 17
β’ Β· = (
Β·π βπ) |
10 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(invgβπ) = (invgβπ) |
11 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(invgβπ
) = (invgβπ
) |
12 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ
) =
(Baseβπ
) |
13 | 7, 8, 9, 10, 11, 12 | lmodvsinv 20512 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β (Baseβπ
) β§ (πΉβπ) β π΅) β (((invgβπ
)βπ) Β· (πΉβπ)) = ((invgβπ)β(π Β· (πΉβπ)))) |
14 | 2, 3, 6, 13 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((invgβπ
)βπ) Β· (πΉβπ)) = ((invgβπ)β(π Β· (πΉβπ)))) |
15 | 14 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β ((invgβπ)β(π Β· (πΉβπ))) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))))) |
16 | | lmodgrp 20343 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β π β Grp) |
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β Grp) |
18 | 7, 8, 9, 12 | lmodvscl 20354 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β (Baseβπ
) β§ (πΉβπ) β π΅) β (π Β· (πΉβπ)) β π΅) |
19 | 2, 3, 6, 18 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Β· (πΉβπ)) β π΅) |
20 | | islindf4.z |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπ) |
21 | | lmodcmn 20385 |
. . . . . . . . . . . . . . . . 17
β’ (π β LMod β π β CMnd) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β CMnd) |
23 | | simpll2 1214 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β πΌ β π) |
24 | | difexg 5285 |
. . . . . . . . . . . . . . . . 17
β’ (πΌ β π β (πΌ β {π}) β V) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (πΌ β {π}) β V) |
26 | | simprlr 779 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π¦ β ((Baseβπ
) βm (πΌ β {π}))) |
27 | | elmapi 8790 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β ((Baseβπ
) βm (πΌ β {π})) β π¦:(πΌ β {π})βΆ(Baseβπ
)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π¦:(πΌ β {π})βΆ(Baseβπ
)) |
29 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β πΉ:πΌβΆπ΅) |
30 | | difss 4092 |
. . . . . . . . . . . . . . . . . 18
β’ (πΌ β {π}) β πΌ |
31 | | fssres 6709 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:πΌβΆπ΅ β§ (πΌ β {π}) β πΌ) β (πΉ βΎ (πΌ β {π})):(πΌ β {π})βΆπ΅) |
32 | 29, 30, 31 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (πΉ βΎ (πΌ β {π})):(πΌ β {π})βΆπ΅) |
33 | 8, 12, 9, 7, 2, 28,
32, 25 | lcomf 20376 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π¦ βf Β· (πΉ βΎ (πΌ β {π}))):(πΌ β {π})βΆπ΅) |
34 | | islindf4.y |
. . . . . . . . . . . . . . . . 17
β’ π = (0gβπ
) |
35 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π¦ finSupp π) |
36 | 8, 12, 9, 7, 2, 28,
32, 25, 20, 34, 35 | lcomfsupp 20377 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π¦ βf Β· (πΉ βΎ (πΌ β {π}))) finSupp 0 ) |
37 | 7, 20, 22, 25, 33, 36 | gsumcl 19697 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π΅) |
38 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(+gβπ) = (+gβπ) |
39 | 7, 38, 20, 10 | grpinvid2 18808 |
. . . . . . . . . . . . . . 15
β’ ((π β Grp β§ (π Β· (πΉβπ)) β π΅ β§ (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π΅) β (((invgβπ)β(π Β· (πΉβπ))) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β ((π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))(+gβπ)(π Β· (πΉβπ))) = 0 )) |
40 | 17, 19, 37, 39 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((invgβπ)β(π Β· (πΉβπ))) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β ((π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))(+gβπ)(π Β· (πΉβπ))) = 0 )) |
41 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β πΌ) |
42 | | fsnunf2 7133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦:(πΌ β {π})βΆ(Baseβπ
) β§ π β πΌ β§ π β (Baseβπ
)) β (π¦ βͺ {β¨π, πβ©}):πΌβΆ(Baseβπ
)) |
43 | 28, 41, 3, 42 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π¦ βͺ {β¨π, πβ©}):πΌβΆ(Baseβπ
)) |
44 | 8, 12, 9, 7, 2, 43,
29, 23 | lcomf 20376 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ):πΌβΆπ΅) |
45 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β π β πΌ) |
46 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β π β (Baseβπ
)) |
47 | 45, 46 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (π β πΌ β§ π β (Baseβπ
))) |
48 | | elmapfun 8807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β ((Baseβπ
) βm (πΌ β {π})) β Fun π¦) |
49 | | fdm 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦:(πΌ β {π})βΆ(Baseβπ
) β dom π¦ = (πΌ β {π})) |
50 | | neldifsnd 4754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (dom
π¦ = (πΌ β {π}) β Β¬ π β (πΌ β {π})) |
51 | | df-nel 3047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β dom π¦ β Β¬ π β dom π¦) |
52 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (dom
π¦ = (πΌ β {π}) β (π β dom π¦ β π β (πΌ β {π}))) |
53 | 52 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (dom
π¦ = (πΌ β {π}) β (Β¬ π β dom π¦ β Β¬ π β (πΌ β {π}))) |
54 | 51, 53 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (dom
π¦ = (πΌ β {π}) β (π β dom π¦ β Β¬ π β (πΌ β {π}))) |
55 | 50, 54 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (dom
π¦ = (πΌ β {π}) β π β dom π¦) |
56 | 27, 49, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β ((Baseβπ
) βm (πΌ β {π})) β π β dom π¦) |
57 | 48, 56 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β ((Baseβπ
) βm (πΌ β {π})) β (Fun π¦ β§ π β dom π¦)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β (Fun π¦ β§ π β dom π¦)) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (Fun π¦ β§ π β dom π¦)) |
60 | 47, 59 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β ((π β πΌ β§ π β (Baseβπ
)) β§ (Fun π¦ β§ π β dom π¦))) |
61 | | funsnfsupp 9334 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β πΌ β§ π β (Baseβπ
)) β§ (Fun π¦ β§ π β dom π¦)) β ((π¦ βͺ {β¨π, πβ©}) finSupp π β π¦ finSupp π)) |
62 | 61 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β πΌ β§ π β (Baseβπ
)) β§ (Fun π¦ β§ π β dom π¦)) β (π¦ finSupp π β (π¦ βͺ {β¨π, πβ©}) finSupp π)) |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (π¦ finSupp π β (π¦ βͺ {β¨π, πβ©}) finSupp π)) |
64 | 63 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (π¦ finSupp π β (π¦ βͺ {β¨π, πβ©}) finSupp π)) |
65 | 64 | impr 456 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π¦ βͺ {β¨π, πβ©}) finSupp π) |
66 | 8, 12, 9, 7, 2, 43,
29, 23, 20, 34, 65 | lcomfsupp 20377 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) finSupp 0 ) |
67 | | disjdifr 4433 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΌ β {π}) β© {π}) = β
|
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((πΌ β {π}) β© {π}) = β
) |
69 | | difsnid 4771 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌ β ((πΌ β {π}) βͺ {π}) = πΌ) |
70 | 69 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΌ β πΌ = ((πΌ β {π}) βͺ {π})) |
71 | 41, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β πΌ = ((πΌ β {π}) βͺ {π})) |
72 | 7, 20, 38, 22, 23, 44, 66, 68, 71 | gsumsplit 19710 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = ((π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π})))(+gβπ)(π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π})))) |
73 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π¦ β V |
74 | | snex 5389 |
. . . . . . . . . . . . . . . . . . . . 21
β’
{β¨π, πβ©} β
V |
75 | 73, 74 | unex 7681 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ βͺ {β¨π, πβ©}) β V |
76 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΉ:πΌβΆπ΅) |
77 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΌ β π) |
78 | 76, 77 | fexd 7178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΉ β V) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β πΉ β V) |
80 | | offres 7917 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ βͺ {β¨π, πβ©}) β V β§ πΉ β V) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π})) = (((π¦ βͺ {β¨π, πβ©}) βΎ (πΌ β {π})) βf Β· (πΉ βΎ (πΌ β {π})))) |
81 | 75, 79, 80 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π})) = (((π¦ βͺ {β¨π, πβ©}) βΎ (πΌ β {π})) βf Β· (πΉ βΎ (πΌ β {π})))) |
82 | 28 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π¦ Fn (πΌ β {π})) |
83 | | neldifsn 4753 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Β¬
π β (πΌ β {π}) |
84 | | fsnunres 7135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ Fn (πΌ β {π}) β§ Β¬ π β (πΌ β {π})) β ((π¦ βͺ {β¨π, πβ©}) βΎ (πΌ β {π})) = π¦) |
85 | 82, 83, 84 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π¦ βͺ {β¨π, πβ©}) βΎ (πΌ β {π})) = π¦) |
86 | 85 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βΎ (πΌ β {π})) βf Β· (πΉ βΎ (πΌ β {π}))) = (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) |
87 | 81, 86 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π})) = (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) |
88 | 87 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π}))) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) |
89 | 44 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) Fn πΌ) |
90 | | fnressn 7105 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) Fn πΌ β§ π β πΌ) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π}) = {β¨π, (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ)β©}) |
91 | 89, 41, 90 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π}) = {β¨π, (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ)β©}) |
92 | 43 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π¦ βͺ {β¨π, πβ©}) Fn πΌ) |
93 | 29 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β πΉ Fn πΌ) |
94 | | fnfvof 7635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ βͺ {β¨π, πβ©}) Fn πΌ β§ πΉ Fn πΌ) β§ (πΌ β π β§ π β πΌ)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ) = (((π¦ βͺ {β¨π, πβ©})βπ) Β· (πΉβπ))) |
95 | 92, 93, 23, 41, 94 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ) = (((π¦ βͺ {β¨π, πβ©})βπ) Β· (πΉβπ))) |
96 | | fndm 6606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ Fn (πΌ β {π}) β dom π¦ = (πΌ β {π})) |
97 | 96 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ Fn (πΌ β {π}) β (π β dom π¦ β π β (πΌ β {π}))) |
98 | 83, 97 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ Fn (πΌ β {π}) β Β¬ π β dom π¦) |
99 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π β V |
100 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π β V |
101 | | fsnunfv 7134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β V β§ π β V β§ Β¬ π β dom π¦) β ((π¦ βͺ {β¨π, πβ©})βπ) = π) |
102 | 99, 100, 101 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
π β dom π¦ β ((π¦ βͺ {β¨π, πβ©})βπ) = π) |
103 | 82, 98, 102 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π¦ βͺ {β¨π, πβ©})βπ) = π) |
104 | 103 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©})βπ) Β· (πΉβπ)) = (π Β· (πΉβπ))) |
105 | 95, 104 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ) = (π Β· (πΉβπ))) |
106 | 105 | opeq2d 4838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β β¨π, (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ)β© = β¨π, (π Β· (πΉβπ))β©) |
107 | 106 | sneqd 4599 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β {β¨π, (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)βπ)β©} = {β¨π, (π Β· (πΉβπ))β©}) |
108 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π Β· (πΉβπ)) β V |
109 | | fmptsn 7114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β V β§ (π Β· (πΉβπ)) β V) β {β¨π, (π Β· (πΉβπ))β©} = (π₯ β {π} β¦ (π Β· (πΉβπ)))) |
110 | 99, 108, 109 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’
{β¨π, (π Β· (πΉβπ))β©} = (π₯ β {π} β¦ (π Β· (πΉβπ))) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β {β¨π, (π Β· (πΉβπ))β©} = (π₯ β {π} β¦ (π Β· (πΉβπ)))) |
112 | 91, 107, 111 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π}) = (π₯ β {π} β¦ (π Β· (πΉβπ)))) |
113 | 112 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π})) = (π Ξ£g (π₯ β {π} β¦ (π Β· (πΉβπ))))) |
114 | | cmnmnd 19584 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β CMnd β π β Mnd) |
115 | 2, 21, 114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β Mnd) |
116 | 99 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π β V) |
117 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β (π Β· (πΉβπ)) = (π Β· (πΉβπ))) |
118 | 7, 117 | gsumsn 19736 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Mnd β§ π β V β§ (π Β· (πΉβπ)) β π΅) β (π Ξ£g (π₯ β {π} β¦ (π Β· (πΉβπ)))) = (π Β· (πΉβπ))) |
119 | 115, 116,
19, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g (π₯ β {π} β¦ (π Β· (πΉβπ)))) = (π Β· (πΉβπ))) |
120 | 113, 119 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π})) = (π Β· (πΉβπ))) |
121 | 88, 120 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ (πΌ β {π})))(+gβπ)(π Ξ£g (((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ) βΎ {π}))) = ((π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))(+gβπ)(π Β· (πΉβπ)))) |
122 | 72, 121 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))(+gβπ)(π Β· (πΉβπ))) = (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ))) |
123 | 122 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))(+gβπ)(π Β· (πΉβπ))) = 0 β (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 )) |
124 | 15, 40, 123 | 3bitrd 305 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β ((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 )) |
125 | 103 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β π = ((π¦ βͺ {β¨π, πβ©})βπ)) |
126 | 125 | eqeq1d 2735 |
. . . . . . . . . . . . 13
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (π = π β ((π¦ βͺ {β¨π, πβ©})βπ) = π)) |
127 | 124, 126 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ ((π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π}))) β§ π¦ finSupp π)) β (((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π = π) β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π))) |
128 | 127 | anassrs 469 |
. . . . . . . . . . 11
β’
(((((π β LMod
β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β§ π¦ finSupp π) β (((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π = π) β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π))) |
129 | 128 | pm5.74da 803 |
. . . . . . . . . 10
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β ((π¦ finSupp π β ((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π = π)) β (π¦ finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
130 | | impexp 452 |
. . . . . . . . . . 11
β’ (((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β (π¦ finSupp π β ((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π = π))) |
131 | 130 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β (π¦ finSupp π β ((((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π})))) β π = π)))) |
132 | 63 | bicomd 222 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β ((π¦ βͺ {β¨π, πβ©}) finSupp π β π¦ finSupp π)) |
133 | 132 | imbi1d 342 |
. . . . . . . . . 10
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)) β (π¦ finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
134 | 129, 131,
133 | 3bitr4d 311 |
. . . . . . . . 9
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ (π β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (πΌ β {π})))) β (((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β ((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
135 | 134 | 2ralbidva 3207 |
. . . . . . . 8
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
136 | | breq1 5109 |
. . . . . . . . . . 11
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β (π₯ finSupp π β (π¦ βͺ {β¨π, πβ©}) finSupp π)) |
137 | | oveq1 7365 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β (π₯ βf Β· πΉ) = ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) |
138 | 137 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β (π Ξ£g (π₯ βf Β· πΉ)) = (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ))) |
139 | 138 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 )) |
140 | | fveq1 6842 |
. . . . . . . . . . . . 13
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β (π₯βπ) = ((π¦ βͺ {β¨π, πβ©})βπ)) |
141 | 140 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β ((π₯βπ) = π β ((π¦ βͺ {β¨π, πβ©})βπ) = π)) |
142 | 139, 141 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β (((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π) β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π))) |
143 | 136, 142 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = (π¦ βͺ {β¨π, πβ©}) β ((π₯ finSupp π β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π)) β ((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
144 | 143 | ralxpmap 8837 |
. . . . . . . . 9
β’ (π β πΌ β (βπ₯ β ((Baseβπ
) βm πΌ)(π₯ finSupp π β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π)) β βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
145 | 144 | adantl 483 |
. . . . . . . 8
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ₯ β ((Baseβπ
) βm πΌ)(π₯ finSupp π β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π)) β βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ βͺ {β¨π, πβ©}) finSupp π β ((π Ξ£g ((π¦ βͺ {β¨π, πβ©}) βf Β· πΉ)) = 0 β ((π¦ βͺ {β¨π, πβ©})βπ) = π)))) |
146 | 135, 145 | bitr4d 282 |
. . . . . . 7
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β βπ₯ β ((Baseβπ
) βm πΌ)(π₯ finSupp π β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π)))) |
147 | | breq1 5109 |
. . . . . . . 8
β’ (π§ = π₯ β (π§ finSupp π β π₯ finSupp π)) |
148 | 147 | ralrab 3652 |
. . . . . . 7
β’
(βπ₯ β
{π§ β
((Baseβπ
)
βm πΌ)
β£ π§ finSupp π} ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π) β βπ₯ β ((Baseβπ
) βm πΌ)(π₯ finSupp π β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
149 | 146, 148 | bitr4di 289 |
. . . . . 6
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β βπ₯ β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
150 | | resima 5972 |
. . . . . . . . . . . . 13
β’ ((πΉ βΎ (πΌ β {π})) β (πΌ β {π})) = (πΉ β (πΌ β {π})) |
151 | 150 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ (πΉ β (πΌ β {π})) = ((πΉ βΎ (πΌ β {π})) β (πΌ β {π})) |
152 | 151 | fveq2i 6846 |
. . . . . . . . . . 11
β’
((LSpanβπ)β(πΉ β (πΌ β {π}))) = ((LSpanβπ)β((πΉ βΎ (πΌ β {π})) β (πΌ β {π}))) |
153 | 152 | eleq2i 2826 |
. . . . . . . . . 10
β’
((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β((πΉ βΎ (πΌ β {π})) β (πΌ β {π})))) |
154 | | eqid 2733 |
. . . . . . . . . . 11
β’
(LSpanβπ) =
(LSpanβπ) |
155 | 76, 30, 31 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (πΉ βΎ (πΌ β {π})):(πΌ β {π})βΆπ΅) |
156 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β π β LMod) |
157 | 24 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΌ β {π}) β V) |
158 | 157 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (πΌ β {π}) β V) |
159 | 154, 7, 12, 8, 34, 9, 155, 156, 158 | ellspd 21224 |
. . . . . . . . . 10
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β ((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β((πΉ βΎ (πΌ β {π})) β (πΌ β {π}))) β βπ¦ β ((Baseβπ
) βm (πΌ β {π}))(π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))))) |
160 | 153, 159 | bitrid 283 |
. . . . . . . . 9
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β ((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ¦ β ((Baseβπ
) βm (πΌ β {π}))(π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))))) |
161 | 160 | imbi1d 342 |
. . . . . . . 8
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β π = π) β (βπ¦ β ((Baseβπ
) βm (πΌ β {π}))(π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π))) |
162 | | r19.23v 3176 |
. . . . . . . 8
β’
(βπ¦ β
((Baseβπ
)
βm (πΌ
β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π) β (βπ¦ β ((Baseβπ
) βm (πΌ β {π}))(π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π)) |
163 | 161, 162 | bitr4di 289 |
. . . . . . 7
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β π = π) β βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π))) |
164 | 163 | ralbidv 3171 |
. . . . . 6
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β (Baseβπ
)((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β π = π) β βπ β (Baseβπ
)βπ¦ β ((Baseβπ
) βm (πΌ β {π}))((π¦ finSupp π β§ (((invgβπ
)βπ) Β· (πΉβπ)) = (π Ξ£g (π¦ βf Β· (πΉ βΎ (πΌ β {π}))))) β π = π))) |
165 | | islindf4.l |
. . . . . . . 8
β’ πΏ = (Baseβ(π
freeLMod πΌ)) |
166 | 8 | fvexi 6857 |
. . . . . . . . . . 11
β’ π
β V |
167 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π
freeLMod πΌ) = (π
freeLMod πΌ) |
168 | | eqid 2733 |
. . . . . . . . . . . 12
β’ {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} = {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} |
169 | 167, 12, 34, 168 | frlmbas 21177 |
. . . . . . . . . . 11
β’ ((π
β V β§ πΌ β π) β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} = (Baseβ(π
freeLMod πΌ))) |
170 | 166, 169 | mpan 689 |
. . . . . . . . . 10
β’ (πΌ β π β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} = (Baseβ(π
freeLMod πΌ))) |
171 | 170 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} = (Baseβ(π
freeLMod πΌ))) |
172 | 171 | adantr 482 |
. . . . . . . 8
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} = (Baseβ(π
freeLMod πΌ))) |
173 | 165, 172 | eqtr4id 2792 |
. . . . . . 7
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β πΏ = {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π}) |
174 | 173 | raleqdv 3312 |
. . . . . 6
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π) β βπ₯ β {π§ β ((Baseβπ
) βm πΌ) β£ π§ finSupp π} ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
175 | 149, 164,
174 | 3bitr4d 311 |
. . . . 5
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β (Baseβπ
)((((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β π = π) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
176 | 1, 175 | bitrid 283 |
. . . 4
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β ((Baseβπ
) β {π}) Β¬ (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
177 | 8 | lmodfgrp 20345 |
. . . . . . . 8
β’ (π β LMod β π
β Grp) |
178 | 12, 34, 11 | grpinvnzcl 18824 |
. . . . . . . 8
β’ ((π
β Grp β§ π β ((Baseβπ
) β {π})) β ((invgβπ
)βπ) β ((Baseβπ
) β {π})) |
179 | 177, 178 | sylan 581 |
. . . . . . 7
β’ ((π β LMod β§ π β ((Baseβπ
) β {π})) β ((invgβπ
)βπ) β ((Baseβπ
) β {π})) |
180 | 12, 34, 11 | grpinvnzcl 18824 |
. . . . . . . . 9
β’ ((π
β Grp β§ π β ((Baseβπ
) β {π})) β ((invgβπ
)βπ) β ((Baseβπ
) β {π})) |
181 | 177, 180 | sylan 581 |
. . . . . . . 8
β’ ((π β LMod β§ π β ((Baseβπ
) β {π})) β ((invgβπ
)βπ) β ((Baseβπ
) β {π})) |
182 | | eldifi 4087 |
. . . . . . . . . 10
β’ (π β ((Baseβπ
) β {π}) β π β (Baseβπ
)) |
183 | 12, 11 | grpinvinv 18819 |
. . . . . . . . . 10
β’ ((π
β Grp β§ π β (Baseβπ
)) β
((invgβπ
)β((invgβπ
)βπ)) = π) |
184 | 177, 182,
183 | syl2an 597 |
. . . . . . . . 9
β’ ((π β LMod β§ π β ((Baseβπ
) β {π})) β ((invgβπ
)β((invgβπ
)βπ)) = π) |
185 | 184 | eqcomd 2739 |
. . . . . . . 8
β’ ((π β LMod β§ π β ((Baseβπ
) β {π})) β π = ((invgβπ
)β((invgβπ
)βπ))) |
186 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = ((invgβπ
)βπ) β ((invgβπ
)βπ) = ((invgβπ
)β((invgβπ
)βπ))) |
187 | 186 | rspceeqv 3596 |
. . . . . . . 8
β’
((((invgβπ
)βπ) β ((Baseβπ
) β {π}) β§ π = ((invgβπ
)β((invgβπ
)βπ))) β βπ β ((Baseβπ
) β {π})π = ((invgβπ
)βπ)) |
188 | 181, 185,
187 | syl2anc 585 |
. . . . . . 7
β’ ((π β LMod β§ π β ((Baseβπ
) β {π})) β βπ β ((Baseβπ
) β {π})π = ((invgβπ
)βπ)) |
189 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = ((invgβπ
)βπ) β (π Β· (πΉβπ)) = (((invgβπ
)βπ) Β· (πΉβπ))) |
190 | 189 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = ((invgβπ
)βπ) β ((π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
191 | 190 | notbid 318 |
. . . . . . . 8
β’ (π = ((invgβπ
)βπ) β (Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β Β¬
(((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
192 | 191 | adantl 483 |
. . . . . . 7
β’ ((π β LMod β§ π = ((invgβπ
)βπ)) β (Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β Β¬
(((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
193 | 179, 188,
192 | ralxfrd 5364 |
. . . . . 6
β’ (π β LMod β
(βπ β
((Baseβπ
) β
{π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ β ((Baseβπ
) β {π}) Β¬ (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
194 | 193 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ β ((Baseβπ
) β {π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ β ((Baseβπ
) β {π}) Β¬ (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
195 | 194 | adantr 482 |
. . . 4
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β ((Baseβπ
) β {π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ β ((Baseβπ
) β {π}) Β¬ (((invgβπ
)βπ) Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
196 | | simplr 768 |
. . . . . . . 8
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ π₯ β πΏ) β π β πΌ) |
197 | 34 | fvexi 6857 |
. . . . . . . . 9
β’ π β V |
198 | 197 | fvconst2 7154 |
. . . . . . . 8
β’ (π β πΌ β ((πΌ Γ {π})βπ) = π) |
199 | 196, 198 | syl 17 |
. . . . . . 7
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ π₯ β πΏ) β ((πΌ Γ {π})βπ) = π) |
200 | 199 | eqeq2d 2744 |
. . . . . 6
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ π₯ β πΏ) β ((π₯βπ) = ((πΌ Γ {π})βπ) β (π₯βπ) = π)) |
201 | 200 | imbi2d 341 |
. . . . 5
β’ ((((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β§ π₯ β πΏ) β (((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)) β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
202 | 201 | ralbidva 3169 |
. . . 4
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = π))) |
203 | 176, 195,
202 | 3bitr4d 311 |
. . 3
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π β πΌ) β (βπ β ((Baseβπ
) β {π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)))) |
204 | 203 | ralbidva 3169 |
. 2
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ β πΌ βπ β ((Baseβπ
) β {π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))) β βπ β πΌ βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)))) |
205 | 7, 9, 154, 8, 12, 34 | islindf2 21236 |
. 2
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ β πΌ βπ β ((Baseβπ
) β {π}) Β¬ (π Β· (πΉβπ)) β ((LSpanβπ)β(πΉ β (πΌ β {π}))))) |
206 | 167, 12, 165 | frlmbasf 21182 |
. . . . . . . 8
β’ ((πΌ β π β§ π₯ β πΏ) β π₯:πΌβΆ(Baseβπ
)) |
207 | 206 | 3ad2antl2 1187 |
. . . . . . 7
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π₯ β πΏ) β π₯:πΌβΆ(Baseβπ
)) |
208 | 207 | ffnd 6670 |
. . . . . 6
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π₯ β πΏ) β π₯ Fn πΌ) |
209 | | fnconstg 6731 |
. . . . . . 7
β’ (π β V β (πΌ Γ {π}) Fn πΌ) |
210 | 197, 209 | ax-mp 5 |
. . . . . 6
β’ (πΌ Γ {π}) Fn πΌ |
211 | | eqfnfv 6983 |
. . . . . 6
β’ ((π₯ Fn πΌ β§ (πΌ Γ {π}) Fn πΌ) β (π₯ = (πΌ Γ {π}) β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ))) |
212 | 208, 210,
211 | sylancl 587 |
. . . . 5
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π₯ β πΏ) β (π₯ = (πΌ Γ {π}) β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ))) |
213 | 212 | imbi2d 341 |
. . . 4
β’ (((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β§ π₯ β πΏ) β (((π Ξ£g (π₯ βf Β· πΉ)) = 0 β π₯ = (πΌ Γ {π})) β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ)))) |
214 | 213 | ralbidva 3169 |
. . 3
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β π₯ = (πΌ Γ {π})) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ)))) |
215 | | r19.21v 3173 |
. . . . 5
β’
(βπ β
πΌ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)) β ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ))) |
216 | 215 | ralbii 3093 |
. . . 4
β’
(βπ₯ β
πΏ βπ β πΌ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)) β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ))) |
217 | | ralcom 3271 |
. . . 4
β’
(βπ₯ β
πΏ βπ β πΌ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)) β βπ β πΌ βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ))) |
218 | 216, 217 | bitr3i 277 |
. . 3
β’
(βπ₯ β
πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β βπ β πΌ (π₯βπ) = ((πΌ Γ {π})βπ)) β βπ β πΌ βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ))) |
219 | 214, 218 | bitrdi 287 |
. 2
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β π₯ = (πΌ Γ {π})) β βπ β πΌ βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β (π₯βπ) = ((πΌ Γ {π})βπ)))) |
220 | 204, 205,
219 | 3bitr4d 311 |
1
β’ ((π β LMod β§ πΌ β π β§ πΉ:πΌβΆπ΅) β (πΉ LIndF π β βπ₯ β πΏ ((π Ξ£g (π₯ βf Β· πΉ)) = 0 β π₯ = (πΌ Γ {π})))) |