Step | Hyp | Ref
| Expression |
1 | | islindf5.t |
. . . 4
β’ (π β π β LMod) |
2 | | islindf5.i |
. . . 4
β’ (π β πΌ β π) |
3 | | islindf5.a |
. . . 4
β’ (π β π΄:πΌβΆπΆ) |
4 | | islindf5.c |
. . . . 5
β’ πΆ = (Baseβπ) |
5 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | islindf5.v |
. . . . 5
β’ Β· = (
Β·π βπ) |
7 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
8 | | eqid 2733 |
. . . . 5
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
9 | | eqid 2733 |
. . . . 5
β’
(Baseβ((Scalarβπ) freeLMod πΌ)) = (Baseβ((Scalarβπ) freeLMod πΌ)) |
10 | 4, 5, 6, 7, 8, 9 | islindf4 21260 |
. . . 4
β’ ((π β LMod β§ πΌ β π β§ π΄:πΌβΆπΆ) β (π΄ LIndF π β βπ¦ β (Baseβ((Scalarβπ) freeLMod πΌ))((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
11 | 1, 2, 3, 10 | syl3anc 1372 |
. . 3
β’ (π β (π΄ LIndF π β βπ¦ β (Baseβ((Scalarβπ) freeLMod πΌ))((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
12 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (π₯ βf Β· π΄) = (π¦ βf Β· π΄)) |
13 | 12 | oveq2d 7374 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g (π¦ βf Β· π΄))) |
14 | | islindf5.e |
. . . . . . . . 9
β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) |
15 | | ovex 7391 |
. . . . . . . . 9
β’ (π Ξ£g
(π¦ βf
Β·
π΄)) β
V |
16 | 13, 14, 15 | fvmpt 6949 |
. . . . . . . 8
β’ (π¦ β π΅ β (πΈβπ¦) = (π Ξ£g (π¦ βf Β· π΄))) |
17 | 16 | adantl 483 |
. . . . . . 7
β’ ((π β§ π¦ β π΅) β (πΈβπ¦) = (π Ξ£g (π¦ βf Β· π΄))) |
18 | 17 | eqeq1d 2735 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β ((πΈβπ¦) = (0gβπ) β (π Ξ£g (π¦ βf Β· π΄)) = (0gβπ))) |
19 | | islindf5.r |
. . . . . . . . . . 11
β’ (π β π
= (Scalarβπ)) |
20 | 5 | lmodring 20344 |
. . . . . . . . . . . 12
β’ (π β LMod β
(Scalarβπ) β
Ring) |
21 | 1, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β (Scalarβπ) β Ring) |
22 | 19, 21 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π β π
β Ring) |
23 | | islindf5.f |
. . . . . . . . . . 11
β’ πΉ = (π
freeLMod πΌ) |
24 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
25 | 23, 24 | frlm0 21176 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΌ β π) β (πΌ Γ {(0gβπ
)}) = (0gβπΉ)) |
26 | 22, 2, 25 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πΌ Γ {(0gβπ
)}) = (0gβπΉ)) |
27 | 19 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π β (0gβπ
) =
(0gβ(Scalarβπ))) |
28 | 27 | sneqd 4599 |
. . . . . . . . . 10
β’ (π β
{(0gβπ
)} =
{(0gβ(Scalarβπ))}) |
29 | 28 | xpeq2d 5664 |
. . . . . . . . 9
β’ (π β (πΌ Γ {(0gβπ
)}) = (πΌ Γ
{(0gβ(Scalarβπ))})) |
30 | 26, 29 | eqtr3d 2775 |
. . . . . . . 8
β’ (π β (0gβπΉ) = (πΌ Γ
{(0gβ(Scalarβπ))})) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π΅) β (0gβπΉ) = (πΌ Γ
{(0gβ(Scalarβπ))})) |
32 | 31 | eqeq2d 2744 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β (π¦ = (0gβπΉ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))}))) |
33 | 18, 32 | imbi12d 345 |
. . . . 5
β’ ((π β§ π¦ β π΅) β (((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)) β ((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
34 | 33 | ralbidva 3169 |
. . . 4
β’ (π β (βπ¦ β π΅ ((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)) β βπ¦ β π΅ ((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
35 | 19 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β (Scalarβπ) = π
) |
36 | 35 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((Scalarβπ) freeLMod πΌ) = (π
freeLMod πΌ)) |
37 | 36, 23 | eqtr4di 2791 |
. . . . . . 7
β’ (π β ((Scalarβπ) freeLMod πΌ) = πΉ) |
38 | 37 | fveq2d 6847 |
. . . . . 6
β’ (π β
(Baseβ((Scalarβπ) freeLMod πΌ)) = (BaseβπΉ)) |
39 | | islindf5.b |
. . . . . 6
β’ π΅ = (BaseβπΉ) |
40 | 38, 39 | eqtr4di 2791 |
. . . . 5
β’ (π β
(Baseβ((Scalarβπ) freeLMod πΌ)) = π΅) |
41 | 40 | raleqdv 3312 |
. . . 4
β’ (π β (βπ¦ β
(Baseβ((Scalarβπ) freeLMod πΌ))((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})) β βπ¦ β π΅ ((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
42 | 34, 41 | bitr4d 282 |
. . 3
β’ (π β (βπ¦ β π΅ ((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)) β βπ¦ β (Baseβ((Scalarβπ) freeLMod πΌ))((π Ξ£g (π¦ βf Β· π΄)) = (0gβπ) β π¦ = (πΌ Γ
{(0gβ(Scalarβπ))})))) |
43 | 11, 42 | bitr4d 282 |
. 2
β’ (π β (π΄ LIndF π β βπ¦ β π΅ ((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)))) |
44 | 23, 39, 4, 6, 14, 1,
2, 19, 3 | frlmup1 21220 |
. . 3
β’ (π β πΈ β (πΉ LMHom π)) |
45 | | lmghm 20507 |
. . 3
β’ (πΈ β (πΉ LMHom π) β πΈ β (πΉ GrpHom π)) |
46 | | eqid 2733 |
. . . 4
β’
(0gβπΉ) = (0gβπΉ) |
47 | 39, 4, 46, 7 | ghmf1 19042 |
. . 3
β’ (πΈ β (πΉ GrpHom π) β (πΈ:π΅β1-1βπΆ β βπ¦ β π΅ ((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)))) |
48 | 44, 45, 47 | 3syl 18 |
. 2
β’ (π β (πΈ:π΅β1-1βπΆ β βπ¦ β π΅ ((πΈβπ¦) = (0gβπ) β π¦ = (0gβπΉ)))) |
49 | 43, 48 | bitr4d 282 |
1
β’ (π β (π΄ LIndF π β πΈ:π΅β1-1βπΆ)) |