Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ (π β (Baseβπ) = (Baseβπ)) |
2 | | eqidd 2734 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
3 | | prdslmodd.y |
. . 3
β’ π = (πXsπ
) |
4 | | prdslmodd.s |
. . 3
β’ (π β π β Ring) |
5 | | prdslmodd.rm |
. . . 4
β’ (π β π
:πΌβΆLMod) |
6 | | prdslmodd.i |
. . . 4
β’ (π β πΌ β π) |
7 | 5, 6 | fexd 7178 |
. . 3
β’ (π β π
β V) |
8 | 3, 4, 7 | prdssca 17343 |
. 2
β’ (π β π = (Scalarβπ)) |
9 | | eqidd 2734 |
. 2
β’ (π β (
Β·π βπ) = ( Β·π
βπ)) |
10 | | eqidd 2734 |
. 2
β’ (π β (Baseβπ) = (Baseβπ)) |
11 | | eqidd 2734 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
12 | | eqidd 2734 |
. 2
β’ (π β (.rβπ) = (.rβπ)) |
13 | | eqidd 2734 |
. 2
β’ (π β (1rβπ) = (1rβπ)) |
14 | | lmodgrp 20343 |
. . . . 5
β’ (π β LMod β π β Grp) |
15 | 14 | ssriv 3949 |
. . . 4
β’ LMod
β Grp |
16 | | fss 6686 |
. . . 4
β’ ((π
:πΌβΆLMod β§ LMod β Grp) β
π
:πΌβΆGrp) |
17 | 5, 15, 16 | sylancl 587 |
. . 3
β’ (π β π
:πΌβΆGrp) |
18 | 3, 6, 4, 17 | prdsgrpd 18862 |
. 2
β’ (π β π β Grp) |
19 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
20 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
21 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
22 | 4 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β Ring) |
23 | 6 | elexd 3464 |
. . . . 5
β’ (π β πΌ β V) |
24 | 23 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
25 | 5 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π
:πΌβΆLMod) |
26 | | simprl 770 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
27 | | simprr 772 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
28 | | prdslmodd.rs |
. . . . 5
β’ ((π β§ π¦ β πΌ) β (Scalarβ(π
βπ¦)) = π) |
29 | 28 | adantlr 714 |
. . . 4
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (Scalarβ(π
βπ¦)) = π) |
30 | 3, 19, 20, 21, 22, 24, 25, 26, 27, 29 | prdsvscacl 20444 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
31 | 30 | 3impb 1116 |
. 2
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π( Β·π
βπ)π) β (Baseβπ)) |
32 | 5 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β (π
βπ¦) β LMod) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π
βπ¦) β LMod) |
34 | | simplr1 1216 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
35 | 28 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π¦ β πΌ) β (Baseβ(Scalarβ(π
βπ¦))) = (Baseβπ)) |
36 | 35 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (Baseβ(Scalarβ(π
βπ¦))) = (Baseβπ)) |
37 | 34, 36 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβ(Scalarβ(π
βπ¦)))) |
38 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β Ring) |
39 | 23 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β πΌ β V) |
40 | 5 | ffnd 6670 |
. . . . . . . 8
β’ (π β π
Fn πΌ) |
41 | 40 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π
Fn πΌ) |
42 | | simplr2 1217 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
43 | | simpr 486 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π¦ β πΌ) |
44 | 3, 19, 38, 39, 41, 42, 43 | prdsbasprj 17359 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
45 | | simplr3 1218 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
46 | 3, 19, 38, 39, 41, 45, 43 | prdsbasprj 17359 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
47 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
βπ¦)) = (Baseβ(π
βπ¦)) |
48 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(π
βπ¦)) = (+gβ(π
βπ¦)) |
49 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβ(π
βπ¦)) = (Scalarβ(π
βπ¦)) |
50 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π β(π
βπ¦)) = ( Β·π
β(π
βπ¦)) |
51 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβ(π
βπ¦))) = (Baseβ(Scalarβ(π
βπ¦))) |
52 | 47, 48, 49, 50, 51 | lmodvsdi 20360 |
. . . . . 6
β’ (((π
βπ¦) β LMod β§ (π β (Baseβ(Scalarβ(π
βπ¦))) β§ (πβπ¦) β (Baseβ(π
βπ¦)) β§ (πβπ¦) β (Baseβ(π
βπ¦)))) β (π( Β·π
β(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
53 | 33, 37, 44, 46, 52 | syl13anc 1373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π( Β·π
β(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
54 | | eqid 2733 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
55 | 3, 19, 38, 39, 41, 42, 45, 54, 43 | prdsplusgfval 17361 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβπ)π)βπ¦) = ((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))) |
56 | 55 | oveq2d 7374 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π( Β·π
β(π
βπ¦))((π(+gβπ)π)βπ¦)) = (π( Β·π
β(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦)))) |
57 | 3, 19, 20, 21, 38, 39, 41, 34, 42, 43 | prdsvscafval 17367 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π( Β·π
βπ)π)βπ¦) = (π( Β·π
β(π
βπ¦))(πβπ¦))) |
58 | 3, 19, 20, 21, 38, 39, 41, 34, 45, 43 | prdsvscafval 17367 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π( Β·π
βπ)π)βπ¦) = (π( Β·π
β(π
βπ¦))(πβπ¦))) |
59 | 57, 58 | oveq12d 7376 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
60 | 53, 56, 59 | 3eqtr4d 2783 |
. . . 4
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π( Β·π
β(π
βπ¦))((π(+gβπ)π)βπ¦)) = (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦))) |
61 | 60 | mpteq2dva 5206 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π¦ β πΌ β¦ (π( Β·π
β(π
βπ¦))((π(+gβπ)π)βπ¦))) = (π¦ β πΌ β¦ (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
62 | 4 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β Ring) |
63 | 23 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
64 | 40 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π
Fn πΌ) |
65 | | simpr1 1195 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
66 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β Grp) |
67 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
68 | | simpr3 1197 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
69 | 19, 54 | grpcl 18761 |
. . . . 5
β’ ((π β Grp β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) β (Baseβπ)) |
70 | 66, 67, 68, 69 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)π) β (Baseβπ)) |
71 | 3, 19, 20, 21, 62, 63, 64, 65, 70 | prdsvscaval 17366 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)(π(+gβπ)π)) = (π¦ β πΌ β¦ (π( Β·π
β(π
βπ¦))((π(+gβπ)π)βπ¦)))) |
72 | 30 | 3adantr3 1172 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
73 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β Ring) |
74 | 23 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
75 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π
:πΌβΆLMod) |
76 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
77 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
78 | 28 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (Scalarβ(π
βπ¦)) = π) |
79 | 3, 19, 20, 21, 73, 74, 75, 76, 77, 78 | prdsvscacl 20444 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
80 | 79 | 3adantr2 1171 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
81 | 3, 19, 62, 63, 64, 72, 80, 54 | prdsplusgval 17360 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π)) = (π¦ β πΌ β¦ (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
82 | 61, 71, 81 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)(π(+gβπ)π)) = ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
83 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β Ring) |
84 | 23 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β πΌ β V) |
85 | 40 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π
Fn πΌ) |
86 | | simplr1 1216 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
87 | | simplr3 1218 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
88 | | simpr 486 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π¦ β πΌ) |
89 | 3, 19, 20, 21, 83, 84, 85, 86, 87, 88 | prdsvscafval 17367 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π( Β·π
βπ)π)βπ¦) = (π( Β·π
β(π
βπ¦))(πβπ¦))) |
90 | | simplr2 1217 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
91 | 3, 19, 20, 21, 83, 84, 85, 90, 87, 88 | prdsvscafval 17367 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π( Β·π
βπ)π)βπ¦) = (π( Β·π
β(π
βπ¦))(πβπ¦))) |
92 | 89, 91 | oveq12d 7376 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
93 | 32 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π
βπ¦) β LMod) |
94 | 35 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (Baseβ(Scalarβ(π
βπ¦))) = (Baseβπ)) |
95 | 86, 94 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβ(Scalarβ(π
βπ¦)))) |
96 | 90, 94 | eleqtrrd 2837 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβ(Scalarβ(π
βπ¦)))) |
97 | 3, 19, 83, 84, 85, 87, 88 | prdsbasprj 17359 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
98 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(Scalarβ(π
βπ¦))) =
(+gβ(Scalarβ(π
βπ¦))) |
99 | 47, 48, 49, 50, 51, 98 | lmodvsdir 20361 |
. . . . . 6
β’ (((π
βπ¦) β LMod β§ (π β (Baseβ(Scalarβ(π
βπ¦))) β§ π β (Baseβ(Scalarβ(π
βπ¦))) β§ (πβπ¦) β (Baseβ(π
βπ¦)))) β ((π(+gβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
100 | 93, 95, 96, 97, 99 | syl13anc 1373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = ((π( Β·π
β(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
101 | 28 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (Scalarβ(π
βπ¦)) = π) |
102 | 101 | fveq2d 6847 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β
(+gβ(Scalarβ(π
βπ¦))) = (+gβπ)) |
103 | 102 | oveqd 7375 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π(+gβ(Scalarβ(π
βπ¦)))π) = (π(+gβπ)π)) |
104 | 103 | oveq1d 7373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = ((π(+gβπ)π)( Β·π
β(π
βπ¦))(πβπ¦))) |
105 | 92, 100, 104 | 3eqtr2rd 2780 |
. . . 4
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβπ)π)( Β·π
β(π
βπ¦))(πβπ¦)) = (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦))) |
106 | 105 | mpteq2dva 5206 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π¦ β πΌ β¦ ((π(+gβπ)π)( Β·π
β(π
βπ¦))(πβπ¦))) = (π¦ β πΌ β¦ (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
107 | 4 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β Ring) |
108 | 23 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
109 | 40 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π
Fn πΌ) |
110 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
111 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
112 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
113 | 21, 112 | ringacl 20004 |
. . . . 5
β’ ((π β Ring β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) β (Baseβπ)) |
114 | 107, 110,
111, 113 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)π) β (Baseβπ)) |
115 | | simpr3 1197 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
116 | 3, 19, 20, 21, 107, 108, 109, 114, 115 | prdsvscaval 17366 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(+gβπ)π)( Β·π
βπ)π) = (π¦ β πΌ β¦ ((π(+gβπ)π)( Β·π
β(π
βπ¦))(πβπ¦)))) |
117 | 79 | 3adantr2 1171 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
118 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π
:πΌβΆLMod) |
119 | 3, 19, 20, 21, 107, 108, 118, 111, 115, 101 | prdsvscacl 20444 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)π) β (Baseβπ)) |
120 | 3, 19, 107, 108, 109, 117, 119, 54 | prdsplusgval 17360 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π)) = (π¦ β πΌ β¦ (((π( Β·π
βπ)π)βπ¦)(+gβ(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
121 | 106, 116,
120 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(+gβπ)π)( Β·π
βπ)π) = ((π( Β·π
βπ)π)(+gβπ)(π( Β·π
βπ)π))) |
122 | 91 | oveq2d 7374 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π( Β·π
β(π
βπ¦))((π( Β·π
βπ)π)βπ¦)) = (π( Β·π
β(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
123 | | eqid 2733 |
. . . . . . 7
β’
(.rβ(Scalarβ(π
βπ¦))) =
(.rβ(Scalarβ(π
βπ¦))) |
124 | 47, 49, 50, 51, 123 | lmodvsass 20362 |
. . . . . 6
β’ (((π
βπ¦) β LMod β§ (π β (Baseβ(Scalarβ(π
βπ¦))) β§ π β (Baseβ(Scalarβ(π
βπ¦))) β§ (πβπ¦) β (Baseβ(π
βπ¦)))) β ((π(.rβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = (π( Β·π
β(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
125 | 93, 95, 96, 97, 124 | syl13anc 1373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(.rβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = (π( Β·π
β(π
βπ¦))(π( Β·π
β(π
βπ¦))(πβπ¦)))) |
126 | 101 | fveq2d 6847 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β
(.rβ(Scalarβ(π
βπ¦))) = (.rβπ)) |
127 | 126 | oveqd 7375 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π(.rβ(Scalarβ(π
βπ¦)))π) = (π(.rβπ)π)) |
128 | 127 | oveq1d 7373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(.rβ(Scalarβ(π
βπ¦)))π)( Β·π
β(π
βπ¦))(πβπ¦)) = ((π(.rβπ)π)( Β·π
β(π
βπ¦))(πβπ¦))) |
129 | 122, 125,
128 | 3eqtr2rd 2780 |
. . . 4
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(.rβπ)π)( Β·π
β(π
βπ¦))(πβπ¦)) = (π( Β·π
β(π
βπ¦))((π( Β·π
βπ)π)βπ¦))) |
130 | 129 | mpteq2dva 5206 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π¦ β πΌ β¦ ((π(.rβπ)π)( Β·π
β(π
βπ¦))(πβπ¦))) = (π¦ β πΌ β¦ (π( Β·π
β(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
131 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
132 | 21, 131 | ringcl 19986 |
. . . . 5
β’ ((π β Ring β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(.rβπ)π) β (Baseβπ)) |
133 | 107, 110,
111, 132 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(.rβπ)π) β (Baseβπ)) |
134 | 3, 19, 20, 21, 107, 108, 109, 133, 115 | prdsvscaval 17366 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(.rβπ)π)( Β·π
βπ)π) = (π¦ β πΌ β¦ ((π(.rβπ)π)( Β·π
β(π
βπ¦))(πβπ¦)))) |
135 | 3, 19, 20, 21, 107, 108, 109, 110, 119 | prdsvscaval 17366 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π( Β·π
βπ)(π(
Β·π βπ)π)) = (π¦ β πΌ β¦ (π( Β·π
β(π
βπ¦))((π( Β·π
βπ)π)βπ¦)))) |
136 | 130, 134,
135 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(.rβπ)π)( Β·π
βπ)π) = (π( Β·π
βπ)(π(
Β·π βπ)π))) |
137 | 28 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β
(1rβ(Scalarβ(π
βπ¦))) = (1rβπ)) |
138 | 137 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β
(1rβ(Scalarβ(π
βπ¦))) = (1rβπ)) |
139 | 138 | oveq1d 7373 |
. . . . 5
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β
((1rβ(Scalarβ(π
βπ¦)))( Β·π
β(π
βπ¦))(πβπ¦)) = ((1rβπ)( Β·π
β(π
βπ¦))(πβπ¦))) |
140 | 32 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β (π
βπ¦) β LMod) |
141 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β π β Ring) |
142 | 23 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β πΌ β V) |
143 | 40 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β π
Fn πΌ) |
144 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β π β (Baseβπ)) |
145 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β π¦ β πΌ) |
146 | 3, 19, 141, 142, 143, 144, 145 | prdsbasprj 17359 |
. . . . . 6
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
147 | | eqid 2733 |
. . . . . . 7
β’
(1rβ(Scalarβ(π
βπ¦))) =
(1rβ(Scalarβ(π
βπ¦))) |
148 | 47, 49, 50, 147 | lmodvs1 20365 |
. . . . . 6
β’ (((π
βπ¦) β LMod β§ (πβπ¦) β (Baseβ(π
βπ¦))) β
((1rβ(Scalarβ(π
βπ¦)))( Β·π
β(π
βπ¦))(πβπ¦)) = (πβπ¦)) |
149 | 140, 146,
148 | syl2anc 585 |
. . . . 5
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β
((1rβ(Scalarβ(π
βπ¦)))( Β·π
β(π
βπ¦))(πβπ¦)) = (πβπ¦)) |
150 | 139, 149 | eqtr3d 2775 |
. . . 4
β’ (((π β§ π β (Baseβπ)) β§ π¦ β πΌ) β ((1rβπ)(
Β·π β(π
βπ¦))(πβπ¦)) = (πβπ¦)) |
151 | 150 | mpteq2dva 5206 |
. . 3
β’ ((π β§ π β (Baseβπ)) β (π¦ β πΌ β¦ ((1rβπ)(
Β·π β(π
βπ¦))(πβπ¦))) = (π¦ β πΌ β¦ (πβπ¦))) |
152 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β π β Ring) |
153 | 23 | adantr 482 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β πΌ β V) |
154 | 40 | adantr 482 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β π
Fn πΌ) |
155 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
156 | 21, 155 | ringidcl 19994 |
. . . . . 6
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
157 | 4, 156 | syl 17 |
. . . . 5
β’ (π β (1rβπ) β (Baseβπ)) |
158 | 157 | adantr 482 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β (1rβπ) β (Baseβπ)) |
159 | | simpr 486 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β π β (Baseβπ)) |
160 | 3, 19, 20, 21, 152, 153, 154, 158, 159 | prdsvscaval 17366 |
. . 3
β’ ((π β§ π β (Baseβπ)) β ((1rβπ)(
Β·π βπ)π) = (π¦ β πΌ β¦ ((1rβπ)(
Β·π β(π
βπ¦))(πβπ¦)))) |
161 | 3, 19, 152, 153, 154, 159 | prdsbasfn 17358 |
. . . 4
β’ ((π β§ π β (Baseβπ)) β π Fn πΌ) |
162 | | dffn5 6902 |
. . . 4
β’ (π Fn πΌ β π = (π¦ β πΌ β¦ (πβπ¦))) |
163 | 161, 162 | sylib 217 |
. . 3
β’ ((π β§ π β (Baseβπ)) β π = (π¦ β πΌ β¦ (πβπ¦))) |
164 | 151, 160,
163 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π β (Baseβπ)) β ((1rβπ)(
Β·π βπ)π) = π) |
165 | 1, 2, 8, 9, 10, 11, 12, 13, 4, 18, 31, 82, 121, 136, 164 | islmodd 20342 |
1
β’ (π β π β LMod) |