Step | Hyp | Ref
| Expression |
1 | | frlmup.f |
. . . 4
β’ πΉ = (π
freeLMod πΌ) |
2 | | frlmup.b |
. . . 4
β’ π΅ = (BaseβπΉ) |
3 | | frlmup.c |
. . . 4
β’ πΆ = (Baseβπ) |
4 | | frlmup.v |
. . . 4
β’ Β· = (
Β·π βπ) |
5 | | frlmup.e |
. . . 4
β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) |
6 | | frlmup.t |
. . . 4
β’ (π β π β LMod) |
7 | | frlmup.i |
. . . 4
β’ (π β πΌ β π) |
8 | | frlmup.r |
. . . 4
β’ (π β π
= (Scalarβπ)) |
9 | | frlmup.a |
. . . 4
β’ (π β π΄:πΌβΆπΆ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | frlmup1 21220 |
. . 3
β’ (π β πΈ β (πΉ LMHom π)) |
11 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
12 | 11 | lmodring 20344 |
. . . . . . 7
β’ (π β LMod β
(Scalarβπ) β
Ring) |
13 | 6, 12 | syl 17 |
. . . . . 6
β’ (π β (Scalarβπ) β Ring) |
14 | 8, 13 | eqeltrd 2834 |
. . . . 5
β’ (π β π
β Ring) |
15 | | eqid 2733 |
. . . . . 6
β’ (π
unitVec πΌ) = (π
unitVec πΌ) |
16 | 15, 1, 2 | uvcff 21213 |
. . . . 5
β’ ((π
β Ring β§ πΌ β π) β (π
unitVec πΌ):πΌβΆπ΅) |
17 | 14, 7, 16 | syl2anc 585 |
. . . 4
β’ (π β (π
unitVec πΌ):πΌβΆπ΅) |
18 | 17 | frnd 6677 |
. . 3
β’ (π β ran (π
unitVec πΌ) β π΅) |
19 | | eqid 2733 |
. . . 4
β’
(LSpanβπΉ) =
(LSpanβπΉ) |
20 | | frlmup.k |
. . . 4
β’ πΎ = (LSpanβπ) |
21 | 2, 19, 20 | lmhmlsp 20525 |
. . 3
β’ ((πΈ β (πΉ LMHom π) β§ ran (π
unitVec πΌ) β π΅) β (πΈ β ((LSpanβπΉ)βran (π
unitVec πΌ))) = (πΎβ(πΈ β ran (π
unitVec πΌ)))) |
22 | 10, 18, 21 | syl2anc 585 |
. 2
β’ (π β (πΈ β ((LSpanβπΉ)βran (π
unitVec πΌ))) = (πΎβ(πΈ β ran (π
unitVec πΌ)))) |
23 | 2, 3 | lmhmf 20510 |
. . . . . 6
β’ (πΈ β (πΉ LMHom π) β πΈ:π΅βΆπΆ) |
24 | 10, 23 | syl 17 |
. . . . 5
β’ (π β πΈ:π΅βΆπΆ) |
25 | 24 | ffnd 6670 |
. . . 4
β’ (π β πΈ Fn π΅) |
26 | | fnima 6632 |
. . . 4
β’ (πΈ Fn π΅ β (πΈ β π΅) = ran πΈ) |
27 | 25, 26 | syl 17 |
. . 3
β’ (π β (πΈ β π΅) = ran πΈ) |
28 | | eqid 2733 |
. . . . . . . 8
β’
(LBasisβπΉ) =
(LBasisβπΉ) |
29 | 1, 15, 28 | frlmlbs 21219 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π) β ran (π
unitVec πΌ) β (LBasisβπΉ)) |
30 | 14, 7, 29 | syl2anc 585 |
. . . . . 6
β’ (π β ran (π
unitVec πΌ) β (LBasisβπΉ)) |
31 | 2, 28, 19 | lbssp 20555 |
. . . . . 6
β’ (ran
(π
unitVec πΌ) β (LBasisβπΉ) β ((LSpanβπΉ)βran (π
unitVec πΌ)) = π΅) |
32 | 30, 31 | syl 17 |
. . . . 5
β’ (π β ((LSpanβπΉ)βran (π
unitVec πΌ)) = π΅) |
33 | 32 | eqcomd 2739 |
. . . 4
β’ (π β π΅ = ((LSpanβπΉ)βran (π
unitVec πΌ))) |
34 | 33 | imaeq2d 6014 |
. . 3
β’ (π β (πΈ β π΅) = (πΈ β ((LSpanβπΉ)βran (π
unitVec πΌ)))) |
35 | 27, 34 | eqtr3d 2775 |
. 2
β’ (π β ran πΈ = (πΈ β ((LSpanβπΉ)βran (π
unitVec πΌ)))) |
36 | | imaco 6204 |
. . . 4
β’ ((πΈ β (π
unitVec πΌ)) β πΌ) = (πΈ β ((π
unitVec πΌ) β πΌ)) |
37 | 9 | ffnd 6670 |
. . . . . . 7
β’ (π β π΄ Fn πΌ) |
38 | 17 | ffnd 6670 |
. . . . . . . 8
β’ (π β (π
unitVec πΌ) Fn πΌ) |
39 | | fnco 6619 |
. . . . . . . 8
β’ ((πΈ Fn π΅ β§ (π
unitVec πΌ) Fn πΌ β§ ran (π
unitVec πΌ) β π΅) β (πΈ β (π
unitVec πΌ)) Fn πΌ) |
40 | 25, 38, 18, 39 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΈ β (π
unitVec πΌ)) Fn πΌ) |
41 | | fvco2 6939 |
. . . . . . . . 9
β’ (((π
unitVec πΌ) Fn πΌ β§ π’ β πΌ) β ((πΈ β (π
unitVec πΌ))βπ’) = (πΈβ((π
unitVec πΌ)βπ’))) |
42 | 38, 41 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π’ β πΌ) β ((πΈ β (π
unitVec πΌ))βπ’) = (πΈβ((π
unitVec πΌ)βπ’))) |
43 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β πΌ) β π β LMod) |
44 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β πΌ) β πΌ β π) |
45 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β πΌ) β π
= (Scalarβπ)) |
46 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β πΌ) β π΄:πΌβΆπΆ) |
47 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π’ β πΌ) β π’ β πΌ) |
48 | 1, 2, 3, 4, 5, 43,
44, 45, 46, 47, 15 | frlmup2 21221 |
. . . . . . . 8
β’ ((π β§ π’ β πΌ) β (πΈβ((π
unitVec πΌ)βπ’)) = (π΄βπ’)) |
49 | 42, 48 | eqtr2d 2774 |
. . . . . . 7
β’ ((π β§ π’ β πΌ) β (π΄βπ’) = ((πΈ β (π
unitVec πΌ))βπ’)) |
50 | 37, 40, 49 | eqfnfvd 6986 |
. . . . . 6
β’ (π β π΄ = (πΈ β (π
unitVec πΌ))) |
51 | 50 | imaeq1d 6013 |
. . . . 5
β’ (π β (π΄ β πΌ) = ((πΈ β (π
unitVec πΌ)) β πΌ)) |
52 | | fnima 6632 |
. . . . . 6
β’ (π΄ Fn πΌ β (π΄ β πΌ) = ran π΄) |
53 | 37, 52 | syl 17 |
. . . . 5
β’ (π β (π΄ β πΌ) = ran π΄) |
54 | 51, 53 | eqtr3d 2775 |
. . . 4
β’ (π β ((πΈ β (π
unitVec πΌ)) β πΌ) = ran π΄) |
55 | | fnima 6632 |
. . . . . 6
β’ ((π
unitVec πΌ) Fn πΌ β ((π
unitVec πΌ) β πΌ) = ran (π
unitVec πΌ)) |
56 | 38, 55 | syl 17 |
. . . . 5
β’ (π β ((π
unitVec πΌ) β πΌ) = ran (π
unitVec πΌ)) |
57 | 56 | imaeq2d 6014 |
. . . 4
β’ (π β (πΈ β ((π
unitVec πΌ) β πΌ)) = (πΈ β ran (π
unitVec πΌ))) |
58 | 36, 54, 57 | 3eqtr3a 2797 |
. . 3
β’ (π β ran π΄ = (πΈ β ran (π
unitVec πΌ))) |
59 | 58 | fveq2d 6847 |
. 2
β’ (π β (πΎβran π΄) = (πΎβ(πΈ β ran (π
unitVec πΌ)))) |
60 | 22, 35, 59 | 3eqtr4d 2783 |
1
β’ (π β ran πΈ = (πΎβran π΄)) |