Step | Hyp | Ref
| Expression |
1 | | frlmup.b |
. 2
β’ π΅ = (BaseβπΉ) |
2 | | eqid 2737 |
. 2
β’ (
Β·π βπΉ) = ( Β·π
βπΉ) |
3 | | frlmup.v |
. 2
β’ Β· = (
Β·π βπ) |
4 | | eqid 2737 |
. 2
β’
(ScalarβπΉ) =
(ScalarβπΉ) |
5 | | eqid 2737 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2737 |
. 2
β’
(Baseβ(ScalarβπΉ)) = (Baseβ(ScalarβπΉ)) |
7 | | frlmup.r |
. . . 4
β’ (π β π
= (Scalarβπ)) |
8 | | frlmup.t |
. . . . 5
β’ (π β π β LMod) |
9 | 5 | lmodring 20346 |
. . . . 5
β’ (π β LMod β
(Scalarβπ) β
Ring) |
10 | 8, 9 | syl 17 |
. . . 4
β’ (π β (Scalarβπ) β Ring) |
11 | 7, 10 | eqeltrd 2838 |
. . 3
β’ (π β π
β Ring) |
12 | | frlmup.i |
. . 3
β’ (π β πΌ β π) |
13 | | frlmup.f |
. . . 4
β’ πΉ = (π
freeLMod πΌ) |
14 | 13 | frlmlmod 21171 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β πΉ β LMod) |
15 | 11, 12, 14 | syl2anc 585 |
. 2
β’ (π β πΉ β LMod) |
16 | 13 | frlmsca 21175 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β π
= (ScalarβπΉ)) |
17 | 11, 12, 16 | syl2anc 585 |
. . 3
β’ (π β π
= (ScalarβπΉ)) |
18 | 7, 17 | eqtr3d 2779 |
. 2
β’ (π β (Scalarβπ) = (ScalarβπΉ)) |
19 | | frlmup.c |
. . 3
β’ πΆ = (Baseβπ) |
20 | | eqid 2737 |
. . 3
β’
(+gβπΉ) = (+gβπΉ) |
21 | | eqid 2737 |
. . 3
β’
(+gβπ) = (+gβπ) |
22 | | lmodgrp 20345 |
. . . 4
β’ (πΉ β LMod β πΉ β Grp) |
23 | 15, 22 | syl 17 |
. . 3
β’ (π β πΉ β Grp) |
24 | | lmodgrp 20345 |
. . . 4
β’ (π β LMod β π β Grp) |
25 | 8, 24 | syl 17 |
. . 3
β’ (π β π β Grp) |
26 | | eleq1w 2821 |
. . . . . . 7
β’ (π§ = π₯ β (π§ β π΅ β π₯ β π΅)) |
27 | 26 | anbi2d 630 |
. . . . . 6
β’ (π§ = π₯ β ((π β§ π§ β π΅) β (π β§ π₯ β π΅))) |
28 | | oveq1 7369 |
. . . . . . . 8
β’ (π§ = π₯ β (π§ βf Β· π΄) = (π₯ βf Β· π΄)) |
29 | 28 | oveq2d 7378 |
. . . . . . 7
β’ (π§ = π₯ β (π Ξ£g (π§ βf Β· π΄)) = (π Ξ£g (π₯ βf Β· π΄))) |
30 | 29 | eleq1d 2823 |
. . . . . 6
β’ (π§ = π₯ β ((π Ξ£g (π§ βf Β· π΄)) β πΆ β (π Ξ£g (π₯ βf Β· π΄)) β πΆ)) |
31 | 27, 30 | imbi12d 345 |
. . . . 5
β’ (π§ = π₯ β (((π β§ π§ β π΅) β (π Ξ£g (π§ βf Β· π΄)) β πΆ) β ((π β§ π₯ β π΅) β (π Ξ£g (π₯ βf Β· π΄)) β πΆ))) |
32 | | eqid 2737 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
33 | | lmodcmn 20386 |
. . . . . . . 8
β’ (π β LMod β π β CMnd) |
34 | 8, 33 | syl 17 |
. . . . . . 7
β’ (π β π β CMnd) |
35 | 34 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β π΅) β π β CMnd) |
36 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β π΅) β πΌ β π) |
37 | 8 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β π β LMod) |
38 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β π₯ β (Baseβπ
)) |
39 | 7 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β (Baseβπ
) =
(Baseβ(Scalarβπ))) |
40 | 39 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
41 | 38, 40 | eleqtrd 2840 |
. . . . . . . 8
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β π₯ β (Baseβ(Scalarβπ))) |
42 | | simprr 772 |
. . . . . . . 8
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β π¦ β πΆ) |
43 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
44 | 19, 5, 3, 43 | lmodvscl 20355 |
. . . . . . . 8
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β πΆ) β (π₯ Β· π¦) β πΆ) |
45 | 37, 41, 42, 44 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π§ β π΅) β§ (π₯ β (Baseβπ
) β§ π¦ β πΆ)) β (π₯ Β· π¦) β πΆ) |
46 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
47 | 13, 46, 1 | frlmbasf 21182 |
. . . . . . . 8
β’ ((πΌ β π β§ π§ β π΅) β π§:πΌβΆ(Baseβπ
)) |
48 | 12, 47 | sylan 581 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β π§:πΌβΆ(Baseβπ
)) |
49 | | frlmup.a |
. . . . . . . 8
β’ (π β π΄:πΌβΆπΆ) |
50 | 49 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β π΄:πΌβΆπΆ) |
51 | | inidm 4183 |
. . . . . . 7
β’ (πΌ β© πΌ) = πΌ |
52 | 45, 48, 50, 36, 36, 51 | off 7640 |
. . . . . 6
β’ ((π β§ π§ β π΅) β (π§ βf Β· π΄):πΌβΆπΆ) |
53 | | ovexd 7397 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β (π§ βf Β· π΄) β V) |
54 | 52 | ffund 6677 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β Fun (π§ βf Β· π΄)) |
55 | | fvexd 6862 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β (0gβπ) β V) |
56 | | eqid 2737 |
. . . . . . . . . . 11
β’
(0gβπ
) = (0gβπ
) |
57 | 13, 56, 1 | frlmbasfsupp 21180 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π§ β π΅) β π§ finSupp (0gβπ
)) |
58 | 12, 57 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π§ β π΅) β π§ finSupp (0gβπ
)) |
59 | 7 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β (0gβπ
) =
(0gβ(Scalarβπ))) |
60 | 59 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β
(0gβ(Scalarβπ)) = (0gβπ
)) |
61 | 60 | breq2d 5122 |
. . . . . . . . . 10
β’ (π β (π§ finSupp
(0gβ(Scalarβπ)) β π§ finSupp (0gβπ
))) |
62 | 61 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β π΅) β (π§ finSupp
(0gβ(Scalarβπ)) β π§ finSupp (0gβπ
))) |
63 | 58, 62 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π§ β π΅) β π§ finSupp
(0gβ(Scalarβπ))) |
64 | 63 | fsuppimpd 9319 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β (π§ supp
(0gβ(Scalarβπ))) β Fin) |
65 | | ssidd 3972 |
. . . . . . . 8
β’ ((π β§ π§ β π΅) β (π§ supp
(0gβ(Scalarβπ))) β (π§ supp
(0gβ(Scalarβπ)))) |
66 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π΅) β§ π€ β πΆ) β π β LMod) |
67 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
68 | 19, 5, 3, 67, 32 | lmod0vs 20371 |
. . . . . . . . 9
β’ ((π β LMod β§ π€ β πΆ) β
((0gβ(Scalarβπ)) Β· π€) = (0gβπ)) |
69 | 66, 68 | sylancom 589 |
. . . . . . . 8
β’ (((π β§ π§ β π΅) β§ π€ β πΆ) β
((0gβ(Scalarβπ)) Β· π€) = (0gβπ)) |
70 | | fvexd 6862 |
. . . . . . . 8
β’ ((π β§ π§ β π΅) β
(0gβ(Scalarβπ)) β V) |
71 | 65, 69, 48, 50, 36, 70 | suppssof1 8135 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β ((π§ βf Β· π΄) supp (0gβπ)) β (π§ supp
(0gβ(Scalarβπ)))) |
72 | | suppssfifsupp 9327 |
. . . . . . 7
β’ ((((π§ βf Β· π΄) β V β§ Fun (π§ βf Β· π΄) β§
(0gβπ)
β V) β§ ((π§ supp
(0gβ(Scalarβπ))) β Fin β§ ((π§ βf Β· π΄) supp (0gβπ)) β (π§ supp
(0gβ(Scalarβπ))))) β (π§ βf Β· π΄) finSupp (0gβπ)) |
73 | 53, 54, 55, 64, 71, 72 | syl32anc 1379 |
. . . . . 6
β’ ((π β§ π§ β π΅) β (π§ βf Β· π΄) finSupp (0gβπ)) |
74 | 19, 32, 35, 36, 52, 73 | gsumcl 19699 |
. . . . 5
β’ ((π β§ π§ β π΅) β (π Ξ£g (π§ βf Β· π΄)) β πΆ) |
75 | 31, 74 | chvarvv 2003 |
. . . 4
β’ ((π β§ π₯ β π΅) β (π Ξ£g (π₯ βf Β· π΄)) β πΆ) |
76 | | frlmup.e |
. . . 4
β’ πΈ = (π₯ β π΅ β¦ (π Ξ£g (π₯ βf Β· π΄))) |
77 | 75, 76 | fmptd 7067 |
. . 3
β’ (π β πΈ:π΅βΆπΆ) |
78 | 34 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π β CMnd) |
79 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β πΌ β π) |
80 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π§ = π¦ β (π§ β π΅ β π¦ β π΅)) |
81 | 80 | anbi2d 630 |
. . . . . . . 8
β’ (π§ = π¦ β ((π β§ π§ β π΅) β (π β§ π¦ β π΅))) |
82 | | oveq1 7369 |
. . . . . . . . 9
β’ (π§ = π¦ β (π§ βf Β· π΄) = (π¦ βf Β· π΄)) |
83 | 82 | feq1d 6658 |
. . . . . . . 8
β’ (π§ = π¦ β ((π§ βf Β· π΄):πΌβΆπΆ β (π¦ βf Β· π΄):πΌβΆπΆ)) |
84 | 81, 83 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π¦ β (((π β§ π§ β π΅) β (π§ βf Β· π΄):πΌβΆπΆ) β ((π β§ π¦ β π΅) β (π¦ βf Β· π΄):πΌβΆπΆ))) |
85 | 84, 52 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β (π¦ βf Β· π΄):πΌβΆπΆ) |
86 | 85 | adantrr 716 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ βf Β· π΄):πΌβΆπΆ) |
87 | 52 | adantrl 715 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π§ βf Β· π΄):πΌβΆπΆ) |
88 | 82 | breq1d 5120 |
. . . . . . . 8
β’ (π§ = π¦ β ((π§ βf Β· π΄) finSupp (0gβπ) β (π¦ βf Β· π΄) finSupp (0gβπ))) |
89 | 81, 88 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π¦ β (((π β§ π§ β π΅) β (π§ βf Β· π΄) finSupp (0gβπ)) β ((π β§ π¦ β π΅) β (π¦ βf Β· π΄) finSupp (0gβπ)))) |
90 | 89, 73 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ π¦ β π΅) β (π¦ βf Β· π΄) finSupp (0gβπ)) |
91 | 90 | adantrr 716 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ βf Β· π΄) finSupp (0gβπ)) |
92 | 73 | adantrl 715 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π§ βf Β· π΄) finSupp (0gβπ)) |
93 | 19, 32, 21, 78, 79, 86, 87, 91, 92 | gsumadd 19707 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π Ξ£g ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))) = ((π Ξ£g (π¦ βf Β· π΄))(+gβπ)(π Ξ£g (π§ βf Β· π΄)))) |
94 | 1, 20 | lmodvacl 20352 |
. . . . . . . 8
β’ ((πΉ β LMod β§ π¦ β π΅ β§ π§ β π΅) β (π¦(+gβπΉ)π§) β π΅) |
95 | 94 | 3expb 1121 |
. . . . . . 7
β’ ((πΉ β LMod β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπΉ)π§) β π΅) |
96 | 15, 95 | sylan 581 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπΉ)π§) β π΅) |
97 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = (π¦(+gβπΉ)π§) β (π₯ βf Β· π΄) = ((π¦(+gβπΉ)π§) βf Β· π΄)) |
98 | 97 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = (π¦(+gβπΉ)π§) β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g ((π¦(+gβπΉ)π§) βf Β· π΄))) |
99 | | ovex 7395 |
. . . . . . 7
β’ (π Ξ£g
((π¦(+gβπΉ)π§) βf Β· π΄)) β V |
100 | 98, 76, 99 | fvmpt 6953 |
. . . . . 6
β’ ((π¦(+gβπΉ)π§) β π΅ β (πΈβ(π¦(+gβπΉ)π§)) = (π Ξ£g ((π¦(+gβπΉ)π§) βf Β· π΄))) |
101 | 96, 100 | syl 17 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (πΈβ(π¦(+gβπΉ)π§)) = (π Ξ£g ((π¦(+gβπΉ)π§) βf Β· π΄))) |
102 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π
β Ring) |
103 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
104 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π§ β π΅) |
105 | | eqid 2737 |
. . . . . . . . 9
β’
(+gβπ
) = (+gβπ
) |
106 | 13, 1, 102, 79, 103, 104, 105, 20 | frlmplusgval 21186 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπΉ)π§) = (π¦ βf
(+gβπ
)π§)) |
107 | 106 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦(+gβπΉ)π§) βf Β· π΄) = ((π¦ βf
(+gβπ
)π§) βf Β· π΄)) |
108 | 13, 46, 1 | frlmbasf 21182 |
. . . . . . . . . . . . 13
β’ ((πΌ β π β§ π¦ β π΅) β π¦:πΌβΆ(Baseβπ
)) |
109 | 12, 108 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΅) β π¦:πΌβΆ(Baseβπ
)) |
110 | 109 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π¦:πΌβΆ(Baseβπ
)) |
111 | 110 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ Fn πΌ) |
112 | 48 | adantrl 715 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π§:πΌβΆ(Baseβπ
)) |
113 | 112 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π§ Fn πΌ) |
114 | 111, 113,
79, 79, 51 | offn 7635 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ βf
(+gβπ
)π§) Fn πΌ) |
115 | 49 | ffnd 6674 |
. . . . . . . . . 10
β’ (π β π΄ Fn πΌ) |
116 | 115 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π΄ Fn πΌ) |
117 | 114, 116,
79, 79, 51 | offn 7635 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦ βf
(+gβπ
)π§) βf Β· π΄) Fn πΌ) |
118 | 85 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΅) β (π¦ βf Β· π΄) Fn πΌ) |
119 | 118 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦ βf Β· π΄) Fn πΌ) |
120 | 52 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΅) β (π§ βf Β· π΄) Fn πΌ) |
121 | 120 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π§ βf Β· π΄) Fn πΌ) |
122 | 119, 121,
79, 79, 51 | offn 7635 |
. . . . . . . 8
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄)) Fn πΌ) |
123 | 7 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β (+gβπ
) =
(+gβ(Scalarβπ))) |
124 | 123 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (+gβπ
) =
(+gβ(Scalarβπ))) |
125 | 124 | oveqd 7379 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦βπ₯)(+gβπ
)(π§βπ₯)) = ((π¦βπ₯)(+gβ(Scalarβπ))(π§βπ₯))) |
126 | 125 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦βπ₯)(+gβπ
)(π§βπ₯)) Β· (π΄βπ₯)) = (((π¦βπ₯)(+gβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯))) |
127 | 8 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β π β LMod) |
128 | 110 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦βπ₯) β (Baseβπ
)) |
129 | 39 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
130 | 128, 129 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦βπ₯) β (Baseβ(Scalarβπ))) |
131 | 112 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π§βπ₯) β (Baseβπ
)) |
132 | 131, 129 | eleqtrd 2840 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π§βπ₯) β (Baseβ(Scalarβπ))) |
133 | 49 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π΄:πΌβΆπΆ) |
134 | 133 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π΄βπ₯) β πΆ) |
135 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
136 | 19, 21, 5, 3, 43, 135 | lmodvsdir 20362 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ ((π¦βπ₯) β (Baseβ(Scalarβπ)) β§ (π§βπ₯) β (Baseβ(Scalarβπ)) β§ (π΄βπ₯) β πΆ)) β (((π¦βπ₯)(+gβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯)) = (((π¦βπ₯) Β· (π΄βπ₯))(+gβπ)((π§βπ₯) Β· (π΄βπ₯)))) |
137 | 127, 130,
132, 134, 136 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦βπ₯)(+gβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯)) = (((π¦βπ₯) Β· (π΄βπ₯))(+gβπ)((π§βπ₯) Β· (π΄βπ₯)))) |
138 | 126, 137 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦βπ₯)(+gβπ
)(π§βπ₯)) Β· (π΄βπ₯)) = (((π¦βπ₯) Β· (π΄βπ₯))(+gβπ)((π§βπ₯) Β· (π΄βπ₯)))) |
139 | 111 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β π¦ Fn πΌ) |
140 | 113 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β π§ Fn πΌ) |
141 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β πΌ β π) |
142 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β π₯ β πΌ) |
143 | | fnfvof 7639 |
. . . . . . . . . . . 12
β’ (((π¦ Fn πΌ β§ π§ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β ((π¦ βf
(+gβπ
)π§)βπ₯) = ((π¦βπ₯)(+gβπ
)(π§βπ₯))) |
144 | 139, 140,
141, 142, 143 | syl22anc 838 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦ βf
(+gβπ
)π§)βπ₯) = ((π¦βπ₯)(+gβπ
)(π§βπ₯))) |
145 | 144 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf
(+gβπ
)π§)βπ₯) Β· (π΄βπ₯)) = (((π¦βπ₯)(+gβπ
)(π§βπ₯)) Β· (π΄βπ₯))) |
146 | 115 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β π΄ Fn πΌ) |
147 | | fnfvof 7639 |
. . . . . . . . . . . 12
β’ (((π¦ Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β ((π¦ βf Β· π΄)βπ₯) = ((π¦βπ₯) Β· (π΄βπ₯))) |
148 | 139, 146,
141, 142, 147 | syl22anc 838 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦ βf Β· π΄)βπ₯) = ((π¦βπ₯) Β· (π΄βπ₯))) |
149 | | fnfvof 7639 |
. . . . . . . . . . . 12
β’ (((π§ Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β ((π§ βf Β· π΄)βπ₯) = ((π§βπ₯) Β· (π΄βπ₯))) |
150 | 140, 146,
141, 142, 149 | syl22anc 838 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β ((π§ βf Β· π΄)βπ₯) = ((π§βπ₯) Β· (π΄βπ₯))) |
151 | 148, 150 | oveq12d 7380 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf Β· π΄)βπ₯)(+gβπ)((π§ βf Β· π΄)βπ₯)) = (((π¦βπ₯) Β· (π΄βπ₯))(+gβπ)((π§βπ₯) Β· (π΄βπ₯)))) |
152 | 138, 145,
151 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf
(+gβπ
)π§)βπ₯) Β· (π΄βπ₯)) = (((π¦ βf Β· π΄)βπ₯)(+gβπ)((π§ βf Β· π΄)βπ₯))) |
153 | 114 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦ βf
(+gβπ
)π§) Fn πΌ) |
154 | | fnfvof 7639 |
. . . . . . . . . 10
β’ ((((π¦ βf
(+gβπ
)π§) Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β (((π¦ βf
(+gβπ
)π§) βf Β· π΄)βπ₯) = (((π¦ βf
(+gβπ
)π§)βπ₯) Β· (π΄βπ₯))) |
155 | 153, 146,
141, 142, 154 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf
(+gβπ
)π§) βf Β· π΄)βπ₯) = (((π¦ βf
(+gβπ
)π§)βπ₯) Β· (π΄βπ₯))) |
156 | 119 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦ βf Β· π΄) Fn πΌ) |
157 | 121 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (π§ βf Β· π΄) Fn πΌ) |
158 | | fnfvof 7639 |
. . . . . . . . . 10
β’ ((((π¦ βf Β· π΄) Fn πΌ β§ (π§ βf Β· π΄) Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β (((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))βπ₯) = (((π¦ βf Β· π΄)βπ₯)(+gβπ)((π§ βf Β· π΄)βπ₯))) |
159 | 156, 157,
141, 142, 158 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))βπ₯) = (((π¦ βf Β· π΄)βπ₯)(+gβπ)((π§ βf Β· π΄)βπ₯))) |
160 | 152, 155,
159 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (((π β§ (π¦ β π΅ β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦ βf
(+gβπ
)π§) βf Β· π΄)βπ₯) = (((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))βπ₯)) |
161 | 117, 122,
160 | eqfnfvd 6990 |
. . . . . . 7
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦ βf
(+gβπ
)π§) βf Β· π΄) = ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))) |
162 | 107, 161 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦(+gβπΉ)π§) βf Β· π΄) = ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄))) |
163 | 162 | oveq2d 7378 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π Ξ£g ((π¦(+gβπΉ)π§) βf Β· π΄)) = (π Ξ£g ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄)))) |
164 | 101, 163 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (πΈβ(π¦(+gβπΉ)π§)) = (π Ξ£g ((π¦ βf Β· π΄) βf
(+gβπ)(π§ βf Β· π΄)))) |
165 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯ βf Β· π΄) = (π¦ βf Β· π΄)) |
166 | 165 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = π¦ β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g (π¦ βf Β· π΄))) |
167 | | ovex 7395 |
. . . . . . 7
β’ (π Ξ£g
(π¦ βf
Β·
π΄)) β
V |
168 | 166, 76, 167 | fvmpt 6953 |
. . . . . 6
β’ (π¦ β π΅ β (πΈβπ¦) = (π Ξ£g (π¦ βf Β· π΄))) |
169 | 168 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (πΈβπ¦) = (π Ξ£g (π¦ βf Β· π΄))) |
170 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ βf Β· π΄) = (π§ βf Β· π΄)) |
171 | 170 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = π§ β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g (π§ βf Β· π΄))) |
172 | | ovex 7395 |
. . . . . . 7
β’ (π Ξ£g
(π§ βf
Β·
π΄)) β
V |
173 | 171, 76, 172 | fvmpt 6953 |
. . . . . 6
β’ (π§ β π΅ β (πΈβπ§) = (π Ξ£g (π§ βf Β· π΄))) |
174 | 173 | ad2antll 728 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (πΈβπ§) = (π Ξ£g (π§ βf Β· π΄))) |
175 | 169, 174 | oveq12d 7380 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((πΈβπ¦)(+gβπ)(πΈβπ§)) = ((π Ξ£g (π¦ βf Β· π΄))(+gβπ)(π Ξ£g (π§ βf Β· π΄)))) |
176 | 93, 164, 175 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (πΈβ(π¦(+gβπΉ)π§)) = ((πΈβπ¦)(+gβπ)(πΈβπ§))) |
177 | 1, 19, 20, 21, 23, 25, 77, 176 | isghmd 19024 |
. 2
β’ (π β πΈ β (πΉ GrpHom π)) |
178 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π β LMod) |
179 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β πΌ β π) |
180 | 18 | fveq2d 6851 |
. . . . . . . 8
β’ (π β
(Baseβ(Scalarβπ)) = (Baseβ(ScalarβπΉ))) |
181 | 180 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π¦ β (Baseβ(Scalarβπ)) β π¦ β (Baseβ(ScalarβπΉ)))) |
182 | 181 | biimpar 479 |
. . . . . 6
β’ ((π β§ π¦ β (Baseβ(ScalarβπΉ))) β π¦ β (Baseβ(Scalarβπ))) |
183 | 182 | adantrr 716 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π¦ β (Baseβ(Scalarβπ))) |
184 | 52 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π§ βf Β· π΄):πΌβΆπΆ) |
185 | 184 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π§ βf Β· π΄)βπ₯) β πΆ) |
186 | 52 | feqmptd 6915 |
. . . . . . 7
β’ ((π β§ π§ β π΅) β (π§ βf Β· π΄) = (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯))) |
187 | 186, 73 | eqbrtrrd 5134 |
. . . . . 6
β’ ((π β§ π§ β π΅) β (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯)) finSupp (0gβπ)) |
188 | 187 | adantrl 715 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯)) finSupp (0gβπ)) |
189 | 19, 5, 43, 32, 21, 3, 178, 179, 183, 185, 188 | gsumvsmul 20402 |
. . . 4
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π Ξ£g (π₯ β πΌ β¦ (π¦ Β· ((π§ βf Β· π΄)βπ₯)))) = (π¦ Β· (π Ξ£g (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯))))) |
190 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β πΉ β LMod) |
191 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π¦ β (Baseβ(ScalarβπΉ))) |
192 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π§ β π΅) |
193 | 1, 4, 2, 6 | lmodvscl 20355 |
. . . . . . . . . . . 12
β’ ((πΉ β LMod β§ π¦ β
(Baseβ(ScalarβπΉ)) β§ π§ β π΅) β (π¦( Β·π
βπΉ)π§) β π΅) |
194 | 190, 191,
192, 193 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π¦( Β·π
βπΉ)π§) β π΅) |
195 | 13, 46, 1 | frlmbasf 21182 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ (π¦( Β·π
βπΉ)π§) β π΅) β (π¦( Β·π
βπΉ)π§):πΌβΆ(Baseβπ
)) |
196 | 179, 194,
195 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π¦( Β·π
βπΉ)π§):πΌβΆ(Baseβπ
)) |
197 | 196 | ffnd 6674 |
. . . . . . . . 9
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π¦( Β·π
βπΉ)π§) Fn πΌ) |
198 | 115 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π΄ Fn πΌ) |
199 | 197, 198,
179, 179, 51 | offn 7635 |
. . . . . . . 8
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β ((π¦( Β·π
βπΉ)π§) βf Β· π΄) Fn πΌ) |
200 | | dffn2 6675 |
. . . . . . . 8
β’ (((π¦(
Β·π βπΉ)π§) βf Β· π΄) Fn πΌ β ((π¦( Β·π
βπΉ)π§) βf Β· π΄):πΌβΆV) |
201 | 199, 200 | sylib 217 |
. . . . . . 7
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β ((π¦( Β·π
βπΉ)π§) βf Β· π΄):πΌβΆV) |
202 | 201 | feqmptd 6915 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β ((π¦( Β·π
βπΉ)π§) βf Β· π΄) = (π₯ β πΌ β¦ (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯))) |
203 | 7 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β (.rβπ
) =
(.rβ(Scalarβπ))) |
204 | 203 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (.rβπ
) =
(.rβ(Scalarβπ))) |
205 | 204 | oveqd 7379 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦(.rβπ
)(π§βπ₯)) = (π¦(.rβ(Scalarβπ))(π§βπ₯))) |
206 | 205 | oveq1d 7377 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦(.rβπ
)(π§βπ₯)) Β· (π΄βπ₯)) = ((π¦(.rβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯))) |
207 | 8 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π β LMod) |
208 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π¦ β (Baseβ(ScalarβπΉ))) |
209 | 180 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (Baseβ(Scalarβπ)) =
(Baseβ(ScalarβπΉ))) |
210 | 208, 209 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π¦ β (Baseβ(Scalarβπ))) |
211 | 48 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π΅) β§ π₯ β πΌ) β (π§βπ₯) β (Baseβπ
)) |
212 | 39 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π΅) β§ π₯ β πΌ) β (Baseβπ
) = (Baseβ(Scalarβπ))) |
213 | 211, 212 | eleqtrd 2840 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π΅) β§ π₯ β πΌ) β (π§βπ₯) β (Baseβ(Scalarβπ))) |
214 | 213 | adantlrl 719 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (π§βπ₯) β (Baseβ(Scalarβπ))) |
215 | 49 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΌ) β (π΄βπ₯) β πΆ) |
216 | 215 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (π΄βπ₯) β πΆ) |
217 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
218 | 19, 5, 3, 43, 217 | lmodvsass 20363 |
. . . . . . . . . 10
β’ ((π β LMod β§ (π¦ β
(Baseβ(Scalarβπ)) β§ (π§βπ₯) β (Baseβ(Scalarβπ)) β§ (π΄βπ₯) β πΆ)) β ((π¦(.rβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯)) = (π¦ Β· ((π§βπ₯) Β· (π΄βπ₯)))) |
219 | 207, 210,
214, 216, 218 | syl13anc 1373 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦(.rβ(Scalarβπ))(π§βπ₯)) Β· (π΄βπ₯)) = (π¦ Β· ((π§βπ₯) Β· (π΄βπ₯)))) |
220 | 206, 219 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦(.rβπ
)(π§βπ₯)) Β· (π΄βπ₯)) = (π¦ Β· ((π§βπ₯) Β· (π΄βπ₯)))) |
221 | 197 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦( Β·π
βπΉ)π§) Fn πΌ) |
222 | 115 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π΄ Fn πΌ) |
223 | 12 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β πΌ β π) |
224 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π₯ β πΌ) |
225 | | fnfvof 7639 |
. . . . . . . . . 10
β’ ((((π¦(
Β·π βπΉ)π§) Fn πΌ β§ π΄ Fn πΌ) β§ (πΌ β π β§ π₯ β πΌ)) β (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯) = (((π¦( Β·π
βπΉ)π§)βπ₯) Β· (π΄βπ₯))) |
226 | 221, 222,
223, 224, 225 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯) = (((π¦( Β·π
βπΉ)π§)βπ₯) Β· (π΄βπ₯))) |
227 | 17 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (Baseβπ
) =
(Baseβ(ScalarβπΉ))) |
228 | 227 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (Baseβπ
) = (Baseβ(ScalarβπΉ))) |
229 | 208, 228 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π¦ β (Baseβπ
)) |
230 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π§ β π΅) |
231 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβπ
) = (.rβπ
) |
232 | 13, 1, 46, 223, 229, 230, 224, 2, 231 | frlmvscaval 21190 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π¦( Β·π
βπΉ)π§)βπ₯) = (π¦(.rβπ
)(π§βπ₯))) |
233 | 232 | oveq1d 7377 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦( Β·π
βπΉ)π§)βπ₯) Β· (π΄βπ₯)) = ((π¦(.rβπ
)(π§βπ₯)) Β· (π΄βπ₯))) |
234 | 226, 233 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯) = ((π¦(.rβπ
)(π§βπ₯)) Β· (π΄βπ₯))) |
235 | 48 | ffnd 6674 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΅) β π§ Fn πΌ) |
236 | 235 | adantrl 715 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β π§ Fn πΌ) |
237 | 236 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β π§ Fn πΌ) |
238 | 237, 222,
223, 224, 149 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β ((π§ βf Β· π΄)βπ₯) = ((π§βπ₯) Β· (π΄βπ₯))) |
239 | 238 | oveq2d 7378 |
. . . . . . . 8
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (π¦ Β· ((π§ βf Β· π΄)βπ₯)) = (π¦ Β· ((π§βπ₯) Β· (π΄βπ₯)))) |
240 | 220, 234,
239 | 3eqtr4d 2787 |
. . . . . . 7
β’ (((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β§ π₯ β πΌ) β (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯) = (π¦ Β· ((π§ βf Β· π΄)βπ₯))) |
241 | 240 | mpteq2dva 5210 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π₯ β πΌ β¦ (((π¦( Β·π
βπΉ)π§) βf Β· π΄)βπ₯)) = (π₯ β πΌ β¦ (π¦ Β· ((π§ βf Β· π΄)βπ₯)))) |
242 | 202, 241 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β ((π¦( Β·π
βπΉ)π§) βf Β· π΄) = (π₯ β πΌ β¦ (π¦ Β· ((π§ βf Β· π΄)βπ₯)))) |
243 | 242 | oveq2d 7378 |
. . . 4
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π Ξ£g ((π¦(
Β·π βπΉ)π§) βf Β· π΄)) = (π Ξ£g (π₯ β πΌ β¦ (π¦ Β· ((π§ βf Β· π΄)βπ₯))))) |
244 | 184 | feqmptd 6915 |
. . . . . 6
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π§ βf Β· π΄) = (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯))) |
245 | 244 | oveq2d 7378 |
. . . . 5
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π Ξ£g (π§ βf Β· π΄)) = (π Ξ£g (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯)))) |
246 | 245 | oveq2d 7378 |
. . . 4
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π¦ Β· (π Ξ£g (π§ βf Β· π΄))) = (π¦ Β· (π Ξ£g (π₯ β πΌ β¦ ((π§ βf Β· π΄)βπ₯))))) |
247 | 189, 243,
246 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π Ξ£g ((π¦(
Β·π βπΉ)π§) βf Β· π΄)) = (π¦ Β· (π Ξ£g (π§ βf Β· π΄)))) |
248 | | oveq1 7369 |
. . . . . 6
β’ (π₯ = (π¦( Β·π
βπΉ)π§) β (π₯ βf Β· π΄) = ((π¦( Β·π
βπΉ)π§) βf Β· π΄)) |
249 | 248 | oveq2d 7378 |
. . . . 5
β’ (π₯ = (π¦( Β·π
βπΉ)π§) β (π Ξ£g (π₯ βf Β· π΄)) = (π Ξ£g ((π¦(
Β·π βπΉ)π§) βf Β· π΄))) |
250 | | ovex 7395 |
. . . . 5
β’ (π Ξ£g
((π¦(
Β·π βπΉ)π§) βf Β· π΄)) β V |
251 | 249, 76, 250 | fvmpt 6953 |
. . . 4
β’ ((π¦(
Β·π βπΉ)π§) β π΅ β (πΈβ(π¦( Β·π
βπΉ)π§)) = (π Ξ£g ((π¦(
Β·π βπΉ)π§) βf Β· π΄))) |
252 | 194, 251 | syl 17 |
. . 3
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (πΈβ(π¦( Β·π
βπΉ)π§)) = (π Ξ£g ((π¦(
Β·π βπΉ)π§) βf Β· π΄))) |
253 | 173 | oveq2d 7378 |
. . . 4
β’ (π§ β π΅ β (π¦ Β· (πΈβπ§)) = (π¦ Β· (π Ξ£g (π§ βf Β· π΄)))) |
254 | 253 | ad2antll 728 |
. . 3
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (π¦ Β· (πΈβπ§)) = (π¦ Β· (π Ξ£g (π§ βf Β· π΄)))) |
255 | 247, 252,
254 | 3eqtr4d 2787 |
. 2
β’ ((π β§ (π¦ β (Baseβ(ScalarβπΉ)) β§ π§ β π΅)) β (πΈβ(π¦( Β·π
βπΉ)π§)) = (π¦ Β· (πΈβπ§))) |
256 | 1, 2, 3, 4, 5, 6, 15, 8, 18, 177, 255 | islmhmd 20516 |
1
β’ (π β πΈ β (πΉ LMHom π)) |