Step | Hyp | Ref
| Expression |
1 | | elmapi 8839 |
. . . . 5
β’ (π΄ β (π
βm π) β π΄:πβΆπ
) |
2 | | fdm 6723 |
. . . . . 6
β’ (π΄:πβΆπ
β dom π΄ = π) |
3 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) = (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))) |
4 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π£ = π₯ β (π΄βπ£) = (π΄βπ₯)) |
5 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π£ = π₯ β π£ = π₯) |
6 | 4, 5 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ (π£ = π₯ β ((π΄βπ£)( Β·π
βπ)π£) = ((π΄βπ₯)( Β·π
βπ)π₯)) |
7 | 6 | adantl 482 |
. . . . . . . . . . . 12
β’ (((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β§ π£ = π₯) β ((π΄βπ£)( Β·π
βπ)π£) = ((π΄βπ₯)( Β·π
βπ)π₯)) |
8 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β π₯ β π) |
9 | | ovex 7438 |
. . . . . . . . . . . . 13
β’ ((π΄βπ₯)( Β·π
βπ)π₯) β V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β ((π΄βπ₯)( Β·π
βπ)π₯) β V) |
11 | 3, 7, 8, 10 | fvmptd 7002 |
. . . . . . . . . . 11
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) = ((π΄βπ₯)( Β·π
βπ)π₯)) |
12 | 11 | neeq1d 3000 |
. . . . . . . . . 10
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β (((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ) β ((π΄βπ₯)( Β·π
βπ)π₯) β (0gβπ))) |
13 | | oveq1 7412 |
. . . . . . . . . . . . 13
β’ ((π΄βπ₯) = (0gβπ) β ((π΄βπ₯)( Β·π
βπ)π₯) = ((0gβπ)( Β·π
βπ)π₯)) |
14 | | simplrr 776 |
. . . . . . . . . . . . . 14
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β π β LMod) |
15 | | elelpwi 4611 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π β§ π β π« (Baseβπ)) β π₯ β (Baseβπ)) |
16 | 15 | expcom 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β π«
(Baseβπ) β
(π₯ β π β π₯ β (Baseβπ))) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β π«
(Baseβπ) β§ π β LMod) β (π₯ β π β π₯ β (Baseβπ))) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β (π₯ β π β π₯ β (Baseβπ))) |
19 | 18 | imp 407 |
. . . . . . . . . . . . . 14
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β π₯ β (Baseβπ)) |
20 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
21 | | scmsuppss.s |
. . . . . . . . . . . . . . 15
β’ π = (Scalarβπ) |
22 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (
Β·π βπ) = ( Β·π
βπ) |
23 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(0gβπ) = (0gβπ) |
24 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
(0gβπ) = (0gβπ) |
25 | 20, 21, 22, 23, 24 | lmod0vs 20497 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π₯ β (Baseβπ)) β
((0gβπ)(
Β·π βπ)π₯) = (0gβπ)) |
26 | 14, 19, 25 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β ((0gβπ)(
Β·π βπ)π₯) = (0gβπ)) |
27 | 13, 26 | sylan9eqr 2794 |
. . . . . . . . . . . 12
β’ (((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β§ (π΄βπ₯) = (0gβπ)) β ((π΄βπ₯)( Β·π
βπ)π₯) = (0gβπ)) |
28 | 27 | ex 413 |
. . . . . . . . . . 11
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β ((π΄βπ₯) = (0gβπ) β ((π΄βπ₯)( Β·π
βπ)π₯) = (0gβπ))) |
29 | 28 | necon3d 2961 |
. . . . . . . . . 10
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β (((π΄βπ₯)( Β·π
βπ)π₯) β (0gβπ) β (π΄βπ₯) β (0gβπ))) |
30 | 12, 29 | sylbid 239 |
. . . . . . . . 9
β’ ((((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β§ π₯ β π) β (((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ) β (π΄βπ₯) β (0gβπ))) |
31 | 30 | ss2rabdv 4072 |
. . . . . . . 8
β’ (((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β π β£ (π΄βπ₯) β (0gβπ)}) |
32 | | ovex 7438 |
. . . . . . . . . . . . 13
β’ ((π΄βπ£)( Β·π
βπ)π£) β V |
33 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) = (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) |
34 | 32, 33 | dmmpti 6691 |
. . . . . . . . . . . 12
β’ dom
(π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) = π |
35 | | rabeq 3446 |
. . . . . . . . . . . 12
β’ (dom
(π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) = π β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} = {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)}) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . . . 11
β’ (dom
π΄ = π β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} = {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)}) |
37 | | rabeq 3446 |
. . . . . . . . . . 11
β’ (dom
π΄ = π β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)} = {π₯ β π β£ (π΄βπ₯) β (0gβπ)}) |
38 | 36, 37 | sseq12d 4014 |
. . . . . . . . . 10
β’ (dom
π΄ = π β ({π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)} β {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β π β£ (π΄βπ₯) β (0gβπ)})) |
39 | 38 | adantr 481 |
. . . . . . . . 9
β’ ((dom
π΄ = π β§ π΄:πβΆπ
) β ({π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)} β {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β π β£ (π΄βπ₯) β (0gβπ)})) |
40 | 39 | adantr 481 |
. . . . . . . 8
β’ (((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β ({π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)} β {π₯ β π β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β π β£ (π΄βπ₯) β (0gβπ)})) |
41 | 31, 40 | mpbird 256 |
. . . . . . 7
β’ (((dom
π΄ = π β§ π΄:πβΆπ
) β§ (π β π« (Baseβπ) β§ π β LMod)) β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}) |
42 | 41 | exp43 437 |
. . . . . 6
β’ (dom
π΄ = π β (π΄:πβΆπ
β (π β π« (Baseβπ) β (π β LMod β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)})))) |
43 | 2, 42 | mpcom 38 |
. . . . 5
β’ (π΄:πβΆπ
β (π β π« (Baseβπ) β (π β LMod β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}))) |
44 | 1, 43 | syl 17 |
. . . 4
β’ (π΄ β (π
βm π) β (π β π« (Baseβπ) β (π β LMod β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}))) |
45 | 44 | com13 88 |
. . 3
β’ (π β LMod β (π β π«
(Baseβπ) β
(π΄ β (π
βm π) β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}))) |
46 | 45 | 3imp 1111 |
. 2
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)} β {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}) |
47 | | funmpt 6583 |
. . . 4
β’ Fun
(π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) |
48 | 47 | a1i 11 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β Fun (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))) |
49 | | mptexg 7219 |
. . . 4
β’ (π β π«
(Baseβπ) β
(π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β V) |
50 | 49 | 3ad2ant2 1134 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β V) |
51 | | fvexd 6903 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β (0gβπ) β V) |
52 | | suppval1 8148 |
. . 3
β’ ((Fun
(π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β§ (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β V β§ (0gβπ) β V) β ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) supp (0gβπ)) = {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)}) |
53 | 48, 50, 51, 52 | syl3anc 1371 |
. 2
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) supp (0gβπ)) = {π₯ β dom (π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) β£ ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£))βπ₯) β (0gβπ)}) |
54 | | elmapfun 8856 |
. . . 4
β’ (π΄ β (π
βm π) β Fun π΄) |
55 | 54 | 3ad2ant3 1135 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β Fun π΄) |
56 | | simp3 1138 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β π΄ β (π
βm π)) |
57 | | fvexd 6903 |
. . 3
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β (0gβπ) β V) |
58 | | suppval1 8148 |
. . 3
β’ ((Fun
π΄ β§ π΄ β (π
βm π) β§ (0gβπ) β V) β (π΄ supp (0gβπ)) = {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}) |
59 | 55, 56, 57, 58 | syl3anc 1371 |
. 2
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β (π΄ supp (0gβπ)) = {π₯ β dom π΄ β£ (π΄βπ₯) β (0gβπ)}) |
60 | 46, 53, 59 | 3sstr4d 4028 |
1
β’ ((π β LMod β§ π β π«
(Baseβπ) β§ π΄ β (π
βm π)) β ((π£ β π β¦ ((π΄βπ£)( Β·π
βπ)π£)) supp (0gβπ)) β (π΄ supp (0gβπ))) |