Step | Hyp | Ref
| Expression |
1 | | lspval.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | lspval.s |
. . . . 5
β’ π = (LSubSpβπ) |
3 | | lspval.n |
. . . . 5
β’ π = (LSpanβπ) |
4 | 1, 2, 3 | lspfval 13540 |
. . . 4
β’ (π β LMod β π = (π β π« π β¦ β© {π‘ β π β£ π β π‘})) |
5 | 4 | fveq1d 5529 |
. . 3
β’ (π β LMod β (πβπ) = ((π β π« π β¦ β© {π‘ β π β£ π β π‘})βπ)) |
6 | 5 | adantr 276 |
. 2
β’ ((π β LMod β§ π β π) β (πβπ) = ((π β π« π β¦ β© {π‘ β π β£ π β π‘})βπ)) |
7 | | eqid 2187 |
. . 3
β’ (π β π« π β¦ β© {π‘
β π β£ π β π‘}) = (π β π« π β¦ β© {π‘ β π β£ π β π‘}) |
8 | | sseq1 3190 |
. . . . 5
β’ (π = π β (π β π‘ β π β π‘)) |
9 | 8 | rabbidv 2738 |
. . . 4
β’ (π = π β {π‘ β π β£ π β π‘} = {π‘ β π β£ π β π‘}) |
10 | 9 | inteqd 3861 |
. . 3
β’ (π = π β β© {π‘ β π β£ π β π‘} = β© {π‘ β π β£ π β π‘}) |
11 | | simpr 110 |
. . . 4
β’ ((π β LMod β§ π β π) β π β π) |
12 | | basfn 12533 |
. . . . . . 7
β’ Base Fn
V |
13 | | elex 2760 |
. . . . . . . 8
β’ (π β LMod β π β V) |
14 | 13 | adantr 276 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β π β V) |
15 | | funfvex 5544 |
. . . . . . . 8
β’ ((Fun
Base β§ π β dom
Base) β (Baseβπ)
β V) |
16 | 15 | funfni 5328 |
. . . . . . 7
β’ ((Base Fn
V β§ π β V) β
(Baseβπ) β
V) |
17 | 12, 14, 16 | sylancr 414 |
. . . . . 6
β’ ((π β LMod β§ π β π) β (Baseβπ) β V) |
18 | 1, 17 | eqeltrid 2274 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β V) |
19 | | elpw2g 4168 |
. . . . 5
β’ (π β V β (π β π« π β π β π)) |
20 | 18, 19 | syl 14 |
. . . 4
β’ ((π β LMod β§ π β π) β (π β π« π β π β π)) |
21 | 11, 20 | mpbird 167 |
. . 3
β’ ((π β LMod β§ π β π) β π β π« π) |
22 | 1, 2 | lss1 13514 |
. . . . 5
β’ (π β LMod β π β π) |
23 | | sseq2 3191 |
. . . . . 6
β’ (π‘ = π β (π β π‘ β π β π)) |
24 | 23 | rspcev 2853 |
. . . . 5
β’ ((π β π β§ π β π) β βπ‘ β π π β π‘) |
25 | 22, 24 | sylan 283 |
. . . 4
β’ ((π β LMod β§ π β π) β βπ‘ β π π β π‘) |
26 | | intexrabim 4165 |
. . . 4
β’
(βπ‘ β
π π β π‘ β β© {π‘ β π β£ π β π‘} β V) |
27 | 25, 26 | syl 14 |
. . 3
β’ ((π β LMod β§ π β π) β β© {π‘ β π β£ π β π‘} β V) |
28 | 7, 10, 21, 27 | fvmptd3 5622 |
. 2
β’ ((π β LMod β§ π β π) β ((π β π« π β¦ β© {π‘ β π β£ π β π‘})βπ) = β© {π‘ β π β£ π β π‘}) |
29 | 6, 28 | eqtrd 2220 |
1
β’ ((π β LMod β§ π β π) β (πβπ) = β© {π‘ β π β£ π β π‘}) |