Step | Hyp | Ref
| Expression |
1 | | frlmup.r |
. . . . . 6
β’ (π β π
= (Scalarβπ)) |
2 | | frlmup.t |
. . . . . . 7
β’ (π β π β LMod) |
3 | | eqid 2733 |
. . . . . . . 8
β’
(Scalarβπ) =
(Scalarβπ) |
4 | 3 | lmodring 20344 |
. . . . . . 7
β’ (π β LMod β
(Scalarβπ) β
Ring) |
5 | 2, 4 | syl 17 |
. . . . . 6
β’ (π β (Scalarβπ) β Ring) |
6 | 1, 5 | eqeltrd 2834 |
. . . . 5
β’ (π β π
β Ring) |
7 | | frlmup.i |
. . . . 5
β’ (π β πΌ β π) |
8 | | frlmup.u |
. . . . . 6
β’ π = (π
unitVec πΌ) |
9 | | frlmup.f |
. . . . . 6
β’ πΉ = (π
freeLMod πΌ) |
10 | | frlmup.b |
. . . . . 6
β’ π΅ = (BaseβπΉ) |
11 | 8, 9, 10 | uvcff 21213 |
. . . . 5
β’ ((π
β Ring β§ πΌ β π) β π:πΌβΆπ΅) |
12 | 6, 7, 11 | syl2anc 585 |
. . . 4
β’ (π β π:πΌβΆπ΅) |
13 | | frlmup.y |
. . . 4
β’ (π β π β πΌ) |
14 | 12, 13 | ffvelcdmd 7037 |
. . 3
β’ (π β (πβπ) β π΅) |
15 | | oveq1 7365 |
. . . . 5
β’ (π₯ = (πβπ) β (π₯ βf Β· π΄) = ((πβπ) βf Β· π΄)) |
16 | 15 | oveq2d 7374 |
. . . 4
β’ (π₯ = (πβπ) β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g ((πβπ) βf Β· π΄))) |
17 | | frlmup.e |
. . . 4
β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) |
18 | | ovex 7391 |
. . . 4
β’ (π Ξ£g
((πβπ) βf Β· π΄)) β V |
19 | 16, 17, 18 | fvmpt 6949 |
. . 3
β’ ((πβπ) β π΅ β (πΈβ(πβπ)) = (π Ξ£g ((πβπ) βf Β· π΄))) |
20 | 14, 19 | syl 17 |
. 2
β’ (π β (πΈβ(πβπ)) = (π Ξ£g ((πβπ) βf Β· π΄))) |
21 | | frlmup.c |
. . 3
β’ πΆ = (Baseβπ) |
22 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
23 | | lmodcmn 20385 |
. . . 4
β’ (π β LMod β π β CMnd) |
24 | | cmnmnd 19584 |
. . . 4
β’ (π β CMnd β π β Mnd) |
25 | 2, 23, 24 | 3syl 18 |
. . 3
β’ (π β π β Mnd) |
26 | | eqid 2733 |
. . . 4
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
27 | | frlmup.v |
. . . 4
β’ Β· = (
Β·π βπ) |
28 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ
) =
(Baseβπ
) |
29 | 9, 28, 10 | frlmbasf 21182 |
. . . . . 6
β’ ((πΌ β π β§ (πβπ) β π΅) β (πβπ):πΌβΆ(Baseβπ
)) |
30 | 7, 14, 29 | syl2anc 585 |
. . . . 5
β’ (π β (πβπ):πΌβΆ(Baseβπ
)) |
31 | 1 | fveq2d 6847 |
. . . . . 6
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
32 | 31 | feq3d 6656 |
. . . . 5
β’ (π β ((πβπ):πΌβΆ(Baseβπ
) β (πβπ):πΌβΆ(Baseβ(Scalarβπ)))) |
33 | 30, 32 | mpbid 231 |
. . . 4
β’ (π β (πβπ):πΌβΆ(Baseβ(Scalarβπ))) |
34 | | frlmup.a |
. . . 4
β’ (π β π΄:πΌβΆπΆ) |
35 | 3, 26, 27, 21, 2, 33, 34, 7 | lcomf 20376 |
. . 3
β’ (π β ((πβπ) βf Β· π΄):πΌβΆπΆ) |
36 | 30 | ffnd 6670 |
. . . . . . 7
β’ (π β (πβπ) Fn πΌ) |
37 | 36 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β (πβπ) Fn πΌ) |
38 | 34 | ffnd 6670 |
. . . . . . 7
β’ (π β π΄ Fn πΌ) |
39 | 38 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β π΄ Fn πΌ) |
40 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β πΌ β π) |
41 | | eldifi 4087 |
. . . . . . 7
β’ (π₯ β (πΌ β {π}) β π₯ β πΌ) |
42 | 41 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β π₯ β πΌ) |
43 | | fnfvof 7635 |
. . . . . 6
β’ ((((πβπ) Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β (((πβπ) βf Β· π΄)βπ₯) = (((πβπ)βπ₯) Β· (π΄βπ₯))) |
44 | 37, 39, 40, 42, 43 | syl22anc 838 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β {π})) β (((πβπ) βf Β· π΄)βπ₯) = (((πβπ)βπ₯) Β· (π΄βπ₯))) |
45 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β {π})) β π
β Ring) |
46 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β {π})) β π β πΌ) |
47 | | eldifsni 4751 |
. . . . . . . . . 10
β’ (π₯ β (πΌ β {π}) β π₯ β π) |
48 | 47 | necomd 2996 |
. . . . . . . . 9
β’ (π₯ β (πΌ β {π}) β π β π₯) |
49 | 48 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΌ β {π})) β π β π₯) |
50 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
51 | 8, 45, 40, 46, 42, 49, 50 | uvcvv0 21212 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β {π})) β ((πβπ)βπ₯) = (0gβπ
)) |
52 | 1 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (0gβπ
) =
(0gβ(Scalarβπ))) |
53 | 52 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β (πΌ β {π})) β (0gβπ
) =
(0gβ(Scalarβπ))) |
54 | 51, 53 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β ((πβπ)βπ₯) = (0gβ(Scalarβπ))) |
55 | 54 | oveq1d 7373 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β {π})) β (((πβπ)βπ₯) Β· (π΄βπ₯)) =
((0gβ(Scalarβπ)) Β· (π΄βπ₯))) |
56 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β π β LMod) |
57 | | ffvelcdm 7033 |
. . . . . . 7
β’ ((π΄:πΌβΆπΆ β§ π₯ β πΌ) β (π΄βπ₯) β πΆ) |
58 | 34, 41, 57 | syl2an 597 |
. . . . . 6
β’ ((π β§ π₯ β (πΌ β {π})) β (π΄βπ₯) β πΆ) |
59 | | eqid 2733 |
. . . . . . 7
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
60 | 21, 3, 27, 59, 22 | lmod0vs 20370 |
. . . . . 6
β’ ((π β LMod β§ (π΄βπ₯) β πΆ) β
((0gβ(Scalarβπ)) Β· (π΄βπ₯)) = (0gβπ)) |
61 | 56, 58, 60 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β (πΌ β {π})) β
((0gβ(Scalarβπ)) Β· (π΄βπ₯)) = (0gβπ)) |
62 | 44, 55, 61 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π₯ β (πΌ β {π})) β (((πβπ) βf Β· π΄)βπ₯) = (0gβπ)) |
63 | 35, 62 | suppss 8126 |
. . 3
β’ (π β (((πβπ) βf Β· π΄) supp (0gβπ)) β {π}) |
64 | 21, 22, 25, 7, 13, 35, 63 | gsumpt 19744 |
. 2
β’ (π β (π Ξ£g ((πβπ) βf Β· π΄)) = (((πβπ) βf Β· π΄)βπ)) |
65 | | fnfvof 7635 |
. . . 4
β’ ((((πβπ) Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π β πΌ)) β (((πβπ) βf Β· π΄)βπ) = (((πβπ)βπ) Β· (π΄βπ))) |
66 | 36, 38, 7, 13, 65 | syl22anc 838 |
. . 3
β’ (π β (((πβπ) βf Β· π΄)βπ) = (((πβπ)βπ) Β· (π΄βπ))) |
67 | | eqid 2733 |
. . . . . 6
β’
(1rβπ
) = (1rβπ
) |
68 | 8, 6, 7, 13, 67 | uvcvv1 21211 |
. . . . 5
β’ (π β ((πβπ)βπ) = (1rβπ
)) |
69 | 1 | fveq2d 6847 |
. . . . 5
β’ (π β (1rβπ
) =
(1rβ(Scalarβπ))) |
70 | 68, 69 | eqtrd 2773 |
. . . 4
β’ (π β ((πβπ)βπ) = (1rβ(Scalarβπ))) |
71 | 70 | oveq1d 7373 |
. . 3
β’ (π β (((πβπ)βπ) Β· (π΄βπ)) =
((1rβ(Scalarβπ)) Β· (π΄βπ))) |
72 | 34, 13 | ffvelcdmd 7037 |
. . . 4
β’ (π β (π΄βπ) β πΆ) |
73 | | eqid 2733 |
. . . . 5
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
74 | 21, 3, 27, 73 | lmodvs1 20365 |
. . . 4
β’ ((π β LMod β§ (π΄βπ) β πΆ) β
((1rβ(Scalarβπ)) Β· (π΄βπ)) = (π΄βπ)) |
75 | 2, 72, 74 | syl2anc 585 |
. . 3
β’ (π β
((1rβ(Scalarβπ)) Β· (π΄βπ)) = (π΄βπ)) |
76 | 66, 71, 75 | 3eqtrd 2777 |
. 2
β’ (π β (((πβπ) βf Β· π΄)βπ) = (π΄βπ)) |
77 | 20, 64, 76 | 3eqtrd 2777 |
1
β’ (π β (πΈβ(πβπ)) = (π΄βπ)) |