Step | Hyp | Ref
| Expression |
1 | | lfl0f.o |
. . . . 5
β’ 0 =
(0gβπ·) |
2 | 1 | fvexi 6857 |
. . . 4
β’ 0 β
V |
3 | 2 | fconst 6729 |
. . 3
β’ (π Γ { 0 }):πβΆ{ 0 } |
4 | | lfl0f.d |
. . . . 5
β’ π· = (Scalarβπ) |
5 | | eqid 2733 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
6 | 4, 5, 1 | lmod0cl 20363 |
. . . 4
β’ (π β LMod β 0 β
(Baseβπ·)) |
7 | 6 | snssd 4770 |
. . 3
β’ (π β LMod β { 0 } β
(Baseβπ·)) |
8 | | fss 6686 |
. . 3
β’ (((π Γ { 0 }):πβΆ{ 0 } β§ { 0 } β
(Baseβπ·)) β
(π Γ { 0 }):πβΆ(Baseβπ·)) |
9 | 3, 7, 8 | sylancr 588 |
. 2
β’ (π β LMod β (π Γ { 0 }):πβΆ(Baseβπ·)) |
10 | 4 | lmodring 20344 |
. . . . . . . . 9
β’ (π β LMod β π· β Ring) |
11 | 10 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π· β Ring) |
12 | | simplrl 776 |
. . . . . . . 8
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π β (Baseβπ·)) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ·) = (.rβπ·) |
14 | 5, 13, 1 | ringrz 20017 |
. . . . . . . 8
β’ ((π· β Ring β§ π β (Baseβπ·)) β (π(.rβπ·) 0 ) = 0 ) |
15 | 11, 12, 14 | syl2anc 585 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β (π(.rβπ·) 0 ) = 0 ) |
16 | 15 | oveq1d 7373 |
. . . . . 6
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π(.rβπ·) 0
)(+gβπ·)
0 ) = (
0
(+gβπ·)
0
)) |
17 | | ringgrp 19974 |
. . . . . . . 8
β’ (π· β Ring β π· β Grp) |
18 | 11, 17 | syl 17 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π· β Grp) |
19 | 5, 1 | grpidcl 18783 |
. . . . . . 7
β’ (π· β Grp β 0 β
(Baseβπ·)) |
20 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ·) = (+gβπ·) |
21 | 5, 20, 1 | grplid 18785 |
. . . . . . 7
β’ ((π· β Grp β§ 0 β
(Baseβπ·)) β (
0
(+gβπ·)
0 ) =
0
) |
22 | 18, 19, 21 | syl2anc2 586 |
. . . . . 6
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ( 0 (+gβπ·) 0 ) = 0 ) |
23 | 16, 22 | eqtrd 2773 |
. . . . 5
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π(.rβπ·) 0
)(+gβπ·)
0 ) =
0
) |
24 | | simplrr 777 |
. . . . . . . 8
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π₯ β π) |
25 | 2 | fvconst2 7154 |
. . . . . . . 8
β’ (π₯ β π β ((π Γ { 0 })βπ₯) = 0 ) |
26 | 24, 25 | syl 17 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π Γ { 0 })βπ₯) = 0 ) |
27 | 26 | oveq2d 7374 |
. . . . . 6
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β (π(.rβπ·)((π Γ { 0 })βπ₯)) = (π(.rβπ·) 0 )) |
28 | 2 | fvconst2 7154 |
. . . . . . 7
β’ (π¦ β π β ((π Γ { 0 })βπ¦) = 0 ) |
29 | 28 | adantl 483 |
. . . . . 6
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π Γ { 0 })βπ¦) = 0 ) |
30 | 27, 29 | oveq12d 7376 |
. . . . 5
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π(.rβπ·)((π Γ { 0 })βπ₯))(+gβπ·)((π Γ { 0 })βπ¦)) = ((π(.rβπ·) 0
)(+gβπ·)
0
)) |
31 | | simpll 766 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π β LMod) |
32 | | lfl0f.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
33 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
34 | 32, 4, 33, 5 | lmodvscl 20354 |
. . . . . . . 8
β’ ((π β LMod β§ π β (Baseβπ·) β§ π₯ β π) β (π( Β·π
βπ)π₯) β π) |
35 | 31, 12, 24, 34 | syl3anc 1372 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β (π( Β·π
βπ)π₯) β π) |
36 | | simpr 486 |
. . . . . . 7
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β π¦ β π) |
37 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
38 | 32, 37 | lmodvacl 20351 |
. . . . . . 7
β’ ((π β LMod β§ (π(
Β·π βπ)π₯) β π β§ π¦ β π) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) |
39 | 31, 35, 36, 38 | syl3anc 1372 |
. . . . . 6
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π( Β·π
βπ)π₯)(+gβπ)π¦) β π) |
40 | 2 | fvconst2 7154 |
. . . . . 6
β’ (((π(
Β·π βπ)π₯)(+gβπ)π¦) β π β ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = 0 ) |
41 | 39, 40 | syl 17 |
. . . . 5
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = 0 ) |
42 | 23, 30, 41 | 3eqtr4rd 2784 |
. . . 4
β’ (((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β§ π¦ β π) β ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = ((π(.rβπ·)((π Γ { 0 })βπ₯))(+gβπ·)((π Γ { 0 })βπ¦))) |
43 | 42 | ralrimiva 3140 |
. . 3
β’ ((π β LMod β§ (π β (Baseβπ·) β§ π₯ β π)) β βπ¦ β π ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = ((π(.rβπ·)((π Γ { 0 })βπ₯))(+gβπ·)((π Γ { 0 })βπ¦))) |
44 | 43 | ralrimivva 3194 |
. 2
β’ (π β LMod β
βπ β
(Baseβπ·)βπ₯ β π βπ¦ β π ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = ((π(.rβπ·)((π Γ { 0 })βπ₯))(+gβπ·)((π Γ { 0 })βπ¦))) |
45 | | lfl0f.f |
. . 3
β’ πΉ = (LFnlβπ) |
46 | 32, 37, 4, 33, 5, 20, 13, 45 | islfl 37568 |
. 2
β’ (π β LMod β ((π Γ { 0 }) β πΉ β ((π Γ { 0 }):πβΆ(Baseβπ·) β§ βπ β (Baseβπ·)βπ₯ β π βπ¦ β π ((π Γ { 0 })β((π(
Β·π βπ)π₯)(+gβπ)π¦)) = ((π(.rβπ·)((π Γ { 0 })βπ₯))(+gβπ·)((π Γ { 0 })βπ¦))))) |
47 | 9, 44, 46 | mpbir2and 712 |
1
β’ (π β LMod β (π Γ { 0 }) β πΉ) |