Step | Hyp | Ref
| Expression |
1 | | imaslmod.u |
. . 3
β’ (π β π = (πΉ βs π)) |
2 | | imaslmod.v |
. . . 4
β’ π = (Baseβπ) |
3 | 2 | a1i 11 |
. . 3
β’ (π β π = (Baseβπ)) |
4 | | imaslmod.f |
. . 3
β’ (π β πΉ:πβontoβπ΅) |
5 | | imaslmod.l |
. . 3
β’ (π β π β LMod) |
6 | 1, 3, 4, 5 | imasbas 17399 |
. 2
β’ (π β π΅ = (Baseβπ)) |
7 | | eqidd 2734 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
8 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
9 | 1, 3, 4, 5, 8 | imassca 17406 |
. 2
β’ (π β (Scalarβπ) = (Scalarβπ)) |
10 | | eqidd 2734 |
. 2
β’ (π β (
Β·π βπ) = ( Β·π
βπ)) |
11 | | imaslmod.k |
. . 3
β’ π =
(Baseβ(Scalarβπ)) |
12 | 11 | a1i 11 |
. 2
β’ (π β π = (Baseβ(Scalarβπ))) |
13 | | eqidd 2734 |
. 2
β’ (π β
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ))) |
14 | | eqidd 2734 |
. 2
β’ (π β
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ))) |
15 | | eqidd 2734 |
. 2
β’ (π β
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ))) |
16 | 8 | lmodring 20344 |
. . 3
β’ (π β LMod β
(Scalarβπ) β
Ring) |
17 | 5, 16 | syl 17 |
. 2
β’ (π β (Scalarβπ) β Ring) |
18 | | imaslmod.p |
. . . . 5
β’ + =
(+gβπ) |
19 | 18 | a1i 11 |
. . . 4
β’ (π β + =
(+gβπ)) |
20 | | imaslmod.e1 |
. . . 4
β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) |
21 | | lmodgrp 20343 |
. . . . 5
β’ (π β LMod β π β Grp) |
22 | 5, 21 | syl 17 |
. . . 4
β’ (π β π β Grp) |
23 | | imaslmod.o |
. . . 4
β’ 0 =
(0gβπ) |
24 | 1, 3, 19, 4, 20, 22, 23 | imasgrp 18868 |
. . 3
β’ (π β (π β Grp β§ (πΉβ 0 ) =
(0gβπ))) |
25 | 24 | simpld 496 |
. 2
β’ (π β π β Grp) |
26 | | imaslmod.t |
. . . 4
β’ Β· = (
Β·π βπ) |
27 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
28 | | imaslmod.e2 |
. . . 4
β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) |
29 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β π β LMod) |
30 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β π β π) |
31 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β π β§ π β π)) β π β π) |
32 | 2, 8, 26, 11 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π Β· π) β π) |
33 | 29, 30, 31, 32 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β π β§ π β π)) β (π Β· π) β π) |
34 | 1, 3, 4, 5, 8, 11,
26, 27, 28, 33 | imasvscaf 17426 |
. . 3
β’ (π β (
Β·π βπ):(π Γ π΅)βΆπ΅) |
35 | 34 | fovcld 31600 |
. 2
β’ ((π β§ π’ β π β§ π£ β π΅) β (π’( Β·π
βπ)π£) β π΅) |
36 | | simp-5l 784 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π) |
37 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’ β π β§ π£ β π΅ β§ π€ β π΅)) |
38 | 37 | simp1d 1143 |
. . . . . . . 8
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π’ β π) |
39 | 38 | ad2antrr 725 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π’ β π) |
40 | 36, 22 | syl 17 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π β Grp) |
41 | | simplr 768 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π¦ β π) |
42 | | simp-4r 783 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π§ β π) |
43 | 2, 18 | grpcl 18761 |
. . . . . . . 8
β’ ((π β Grp β§ π¦ β π β§ π§ β π) β (π¦ + π§) β π) |
44 | 40, 41, 42, 43 | syl3anc 1372 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π¦ + π§) β π) |
45 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . . 7
β’ ((π β§ π’ β π β§ (π¦ + π§) β π) β (π’( Β·π
βπ)(πΉβ(π¦ + π§))) = (πΉβ(π’ Β· (π¦ + π§)))) |
46 | 36, 39, 44, 45 | syl3anc 1372 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβ(π¦ + π§))) = (πΉβ(π’ Β· (π¦ + π§)))) |
47 | | eqid 2733 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
48 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17419 |
. . . . . . . . 9
β’ ((π β§ π¦ β π β§ π§ β π) β ((πΉβπ¦)(+gβπ)(πΉβπ§)) = (πΉβ(π¦ + π§))) |
49 | 36, 41, 42, 48 | syl3anc 1372 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β ((πΉβπ¦)(+gβπ)(πΉβπ§)) = (πΉβ(π¦ + π§))) |
50 | | simpr 486 |
. . . . . . . . 9
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβπ¦) = π£) |
51 | | simpllr 775 |
. . . . . . . . 9
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβπ§) = π€) |
52 | 50, 51 | oveq12d 7376 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β ((πΉβπ¦)(+gβπ)(πΉβπ§)) = (π£(+gβπ)π€)) |
53 | 49, 52 | eqtr3d 2775 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβ(π¦ + π§)) = (π£(+gβπ)π€)) |
54 | 53 | oveq2d 7374 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβ(π¦ + π§))) = (π’( Β·π
βπ)(π£(+gβπ)π€))) |
55 | 36, 5 | syl 17 |
. . . . . . . 8
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β π β LMod) |
56 | 2, 18, 8, 26, 11 | lmodvsdi 20360 |
. . . . . . . 8
β’ ((π β LMod β§ (π’ β π β§ π¦ β π β§ π§ β π)) β (π’ Β· (π¦ + π§)) = ((π’ Β· π¦) + (π’ Β· π§))) |
57 | 55, 39, 41, 42, 56 | syl13anc 1373 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’ Β· (π¦ + π§)) = ((π’ Β· π¦) + (π’ Β· π§))) |
58 | 57 | fveq2d 6847 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβ(π’ Β· (π¦ + π§))) = (πΉβ((π’ Β· π¦) + (π’ Β· π§)))) |
59 | 46, 54, 58 | 3eqtr3d 2781 |
. . . . 5
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(π£(+gβπ)π€)) = (πΉβ((π’ Β· π¦) + (π’ Β· π§)))) |
60 | 2, 8, 26, 11 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π’ β π β§ π¦ β π) β (π’ Β· π¦) β π) |
61 | 55, 39, 41, 60 | syl3anc 1372 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’ Β· π¦) β π) |
62 | 2, 8, 26, 11 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π’ β π β§ π§ β π) β (π’ Β· π§) β π) |
63 | 55, 39, 42, 62 | syl3anc 1372 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’ Β· π§) β π) |
64 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17419 |
. . . . . 6
β’ ((π β§ (π’ Β· π¦) β π β§ (π’ Β· π§) β π) β ((πΉβ(π’ Β· π¦))(+gβπ)(πΉβ(π’ Β· π§))) = (πΉβ((π’ Β· π¦) + (π’ Β· π§)))) |
65 | 36, 61, 63, 64 | syl3anc 1372 |
. . . . 5
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β ((πΉβ(π’ Β· π¦))(+gβπ)(πΉβ(π’ Β· π§))) = (πΉβ((π’ Β· π¦) + (π’ Β· π§)))) |
66 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . . . 8
β’ ((π β§ π’ β π β§ π¦ β π) β (π’( Β·π
βπ)(πΉβπ¦)) = (πΉβ(π’ Β· π¦))) |
67 | 36, 39, 41, 66 | syl3anc 1372 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβπ¦)) = (πΉβ(π’ Β· π¦))) |
68 | 50 | oveq2d 7374 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβπ¦)) = (π’( Β·π
βπ)π£)) |
69 | 67, 68 | eqtr3d 2775 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβ(π’ Β· π¦)) = (π’( Β·π
βπ)π£)) |
70 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . . . 8
β’ ((π β§ π’ β π β§ π§ β π) β (π’( Β·π
βπ)(πΉβπ§)) = (πΉβ(π’ Β· π§))) |
71 | 36, 39, 42, 70 | syl3anc 1372 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβπ§)) = (πΉβ(π’ Β· π§))) |
72 | 51 | oveq2d 7374 |
. . . . . . 7
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(πΉβπ§)) = (π’( Β·π
βπ)π€)) |
73 | 71, 72 | eqtr3d 2775 |
. . . . . 6
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (πΉβ(π’ Β· π§)) = (π’( Β·π
βπ)π€)) |
74 | 69, 73 | oveq12d 7376 |
. . . . 5
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β ((πΉβ(π’ Β· π¦))(+gβπ)(πΉβ(π’ Β· π§))) = ((π’( Β·π
βπ)π£)(+gβπ)(π’( Β·π
βπ)π€))) |
75 | 59, 65, 74 | 3eqtr2d 2779 |
. . . 4
β’
((((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β§ π¦ β π) β§ (πΉβπ¦) = π£) β (π’( Β·π
βπ)(π£(+gβπ)π€)) = ((π’( Β·π
βπ)π£)(+gβπ)(π’( Β·π
βπ)π€))) |
76 | | simplll 774 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π) |
77 | 37 | simp2d 1144 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π£ β π΅) |
78 | | fofn 6759 |
. . . . . . 7
β’ (πΉ:πβontoβπ΅ β πΉ Fn π) |
79 | 4, 78 | syl 17 |
. . . . . 6
β’ (π β πΉ Fn π) |
80 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π£ β π΅) β π£ β π΅) |
81 | | forn 6760 |
. . . . . . . . 9
β’ (πΉ:πβontoβπ΅ β ran πΉ = π΅) |
82 | 4, 81 | syl 17 |
. . . . . . . 8
β’ (π β ran πΉ = π΅) |
83 | 82 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π΅) β ran πΉ = π΅) |
84 | 80, 83 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ π£ β π΅) β π£ β ran πΉ) |
85 | | fvelrnb 6904 |
. . . . . . 7
β’ (πΉ Fn π β (π£ β ran πΉ β βπ¦ β π (πΉβπ¦) = π£)) |
86 | 85 | biimpa 478 |
. . . . . 6
β’ ((πΉ Fn π β§ π£ β ran πΉ) β βπ¦ β π (πΉβπ¦) = π£) |
87 | 79, 84, 86 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π£ β π΅) β βπ¦ β π (πΉβπ¦) = π£) |
88 | 76, 77, 87 | syl2anc 585 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β βπ¦ β π (πΉβπ¦) = π£) |
89 | 75, 88 | r19.29a 3156 |
. . 3
β’ ((((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(π£(+gβπ)π€)) = ((π’( Β·π
βπ)π£)(+gβπ)(π’( Β·π
βπ)π€))) |
90 | | simpr 486 |
. . . . . 6
β’ ((π β§ π€ β π΅) β π€ β π΅) |
91 | 82 | adantr 482 |
. . . . . 6
β’ ((π β§ π€ β π΅) β ran πΉ = π΅) |
92 | 90, 91 | eleqtrrd 2837 |
. . . . 5
β’ ((π β§ π€ β π΅) β π€ β ran πΉ) |
93 | | fvelrnb 6904 |
. . . . . 6
β’ (πΉ Fn π β (π€ β ran πΉ β βπ§ β π (πΉβπ§) = π€)) |
94 | 93 | biimpa 478 |
. . . . 5
β’ ((πΉ Fn π β§ π€ β ran πΉ) β βπ§ β π (πΉβπ§) = π€) |
95 | 79, 92, 94 | syl2an2r 684 |
. . . 4
β’ ((π β§ π€ β π΅) β βπ§ β π (πΉβπ§) = π€) |
96 | 95 | 3ad2antr3 1191 |
. . 3
β’ ((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β βπ§ β π (πΉβπ§) = π€) |
97 | 89, 96 | r19.29a 3156 |
. 2
β’ ((π β§ (π’ β π β§ π£ β π΅ β§ π€ β π΅)) β (π’( Β·π
βπ)(π£(+gβπ)π€)) = ((π’( Β·π
βπ)π£)(+gβπ)(π’( Β·π
βπ)π€))) |
98 | | simplll 774 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π) |
99 | 5 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π β LMod) |
100 | | simpllr 775 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’ β π β§ π£ β π β§ π€ β π΅)) |
101 | 100 | simp1d 1143 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π’ β π) |
102 | 100 | simp2d 1144 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π£ β π) |
103 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
104 | 8, 11, 103 | lmodacl 20348 |
. . . . . 6
β’ ((π β LMod β§ π’ β π β§ π£ β π) β (π’(+gβ(Scalarβπ))π£) β π) |
105 | 99, 101, 102, 104 | syl3anc 1372 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’(+gβ(Scalarβπ))π£) β π) |
106 | | simplr 768 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β π§ β π) |
107 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . 5
β’ ((π β§ (π’(+gβ(Scalarβπ))π£) β π β§ π§ β π) β ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = (πΉβ((π’(+gβ(Scalarβπ))π£) Β· π§))) |
108 | 98, 105, 106, 107 | syl3anc 1372 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = (πΉβ((π’(+gβ(Scalarβπ))π£) Β· π§))) |
109 | | simpr 486 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβπ§) = π€) |
110 | 109 | oveq2d 7374 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)π€)) |
111 | 2, 18, 8, 26, 11, 103 | lmodvsdir 20361 |
. . . . . . 7
β’ ((π β LMod β§ (π’ β π β§ π£ β π β§ π§ β π)) β ((π’(+gβ(Scalarβπ))π£) Β· π§) = ((π’ Β· π§) + (π£ Β· π§))) |
112 | 99, 101, 102, 106, 111 | syl13anc 1373 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(+gβ(Scalarβπ))π£) Β· π§) = ((π’ Β· π§) + (π£ Β· π§))) |
113 | 112 | fveq2d 6847 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ((π’(+gβ(Scalarβπ))π£) Β· π§)) = (πΉβ((π’ Β· π§) + (π£ Β· π§)))) |
114 | 99, 101, 106, 62 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’ Β· π§) β π) |
115 | 2, 8, 26, 11 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π£ β π β§ π§ β π) β (π£ Β· π§) β π) |
116 | 99, 102, 106, 115 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π£ Β· π§) β π) |
117 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17419 |
. . . . . 6
β’ ((π β§ (π’ Β· π§) β π β§ (π£ Β· π§) β π) β ((πΉβ(π’ Β· π§))(+gβπ)(πΉβ(π£ Β· π§))) = (πΉβ((π’ Β· π§) + (π£ Β· π§)))) |
118 | 98, 114, 116, 117 | syl3anc 1372 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((πΉβ(π’ Β· π§))(+gβπ)(πΉβ(π£ Β· π§))) = (πΉβ((π’ Β· π§) + (π£ Β· π§)))) |
119 | 98, 101, 106, 70 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(πΉβπ§)) = (πΉβ(π’ Β· π§))) |
120 | 109 | oveq2d 7374 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(πΉβπ§)) = (π’( Β·π
βπ)π€)) |
121 | 119, 120 | eqtr3d 2775 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ(π’ Β· π§)) = (π’( Β·π
βπ)π€)) |
122 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . . . 8
β’ ((π β§ π£ β π β§ π§ β π) β (π£( Β·π
βπ)(πΉβπ§)) = (πΉβ(π£ Β· π§))) |
123 | 98, 102, 106, 122 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π£( Β·π
βπ)(πΉβπ§)) = (πΉβ(π£ Β· π§))) |
124 | 109 | oveq2d 7374 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π£( Β·π
βπ)(πΉβπ§)) = (π£( Β·π
βπ)π€)) |
125 | 123, 124 | eqtr3d 2775 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ(π£ Β· π§)) = (π£( Β·π
βπ)π€)) |
126 | 121, 125 | oveq12d 7376 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((πΉβ(π’ Β· π§))(+gβπ)(πΉβ(π£ Β· π§))) = ((π’( Β·π
βπ)π€)(+gβπ)(π£( Β·π
βπ)π€))) |
127 | 113, 118,
126 | 3eqtr2d 2779 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ((π’(+gβ(Scalarβπ))π£) Β· π§)) = ((π’( Β·π
βπ)π€)(+gβπ)(π£( Β·π
βπ)π€))) |
128 | 108, 110,
127 | 3eqtr3d 2781 |
. . 3
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)π€) = ((π’( Β·π
βπ)π€)(+gβπ)(π£( Β·π
βπ)π€))) |
129 | 95 | 3ad2antr3 1191 |
. . 3
β’ ((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β βπ§ β π (πΉβπ§) = π€) |
130 | 128, 129 | r19.29a 3156 |
. 2
β’ ((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β ((π’(+gβ(Scalarβπ))π£)( Β·π
βπ)π€) = ((π’( Β·π
βπ)π€)(+gβπ)(π£( Β·π
βπ)π€))) |
131 | | eqid 2733 |
. . . . . . . 8
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
132 | 8, 11, 131 | lmodmcl 20349 |
. . . . . . 7
β’ ((π β LMod β§ π’ β π β§ π£ β π) β (π’(.rβ(Scalarβπ))π£) β π) |
133 | 99, 101, 102, 132 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’(.rβ(Scalarβπ))π£) β π) |
134 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . 6
β’ ((π β§ (π’(.rβ(Scalarβπ))π£) β π β§ π§ β π) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = (πΉβ((π’(.rβ(Scalarβπ))π£) Β· π§))) |
135 | 98, 133, 106, 134 | syl3anc 1372 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = (πΉβ((π’(.rβ(Scalarβπ))π£) Β· π§))) |
136 | 109 | oveq2d 7374 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)(πΉβπ§)) = ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)π€)) |
137 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . . . 7
β’ ((π β§ π’ β π β§ (π£ Β· π§) β π) β (π’( Β·π
βπ)(πΉβ(π£ Β· π§))) = (πΉβ(π’ Β· (π£ Β· π§)))) |
138 | 98, 101, 116, 137 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(πΉβ(π£ Β· π§))) = (πΉβ(π’ Β· (π£ Β· π§)))) |
139 | 123 | oveq2d 7374 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(π£(
Β·π βπ)(πΉβπ§))) = (π’( Β·π
βπ)(πΉβ(π£ Β· π§)))) |
140 | 2, 8, 26, 11, 131 | lmodvsass 20362 |
. . . . . . . 8
β’ ((π β LMod β§ (π’ β π β§ π£ β π β§ π§ β π)) β ((π’(.rβ(Scalarβπ))π£) Β· π§) = (π’ Β· (π£ Β· π§))) |
141 | 99, 101, 102, 106, 140 | syl13anc 1373 |
. . . . . . 7
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(.rβ(Scalarβπ))π£) Β· π§) = (π’ Β· (π£ Β· π§))) |
142 | 141 | fveq2d 6847 |
. . . . . 6
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ((π’(.rβ(Scalarβπ))π£) Β· π§)) = (πΉβ(π’ Β· (π£ Β· π§)))) |
143 | 138, 139,
142 | 3eqtr4rd 2784 |
. . . . 5
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (πΉβ((π’(.rβ(Scalarβπ))π£) Β· π§)) = (π’( Β·π
βπ)(π£(
Β·π βπ)(πΉβπ§)))) |
144 | 135, 136,
143 | 3eqtr3d 2781 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)π€) = (π’( Β·π
βπ)(π£(
Β·π βπ)(πΉβπ§)))) |
145 | 124 | oveq2d 7374 |
. . . 4
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β (π’( Β·π
βπ)(π£(
Β·π βπ)(πΉβπ§))) = (π’( Β·π
βπ)(π£(
Β·π βπ)π€))) |
146 | 144, 145 | eqtrd 2773 |
. . 3
β’ ((((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β§ π§ β π) β§ (πΉβπ§) = π€) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)π€) = (π’( Β·π
βπ)(π£(
Β·π βπ)π€))) |
147 | 146, 129 | r19.29a 3156 |
. 2
β’ ((π β§ (π’ β π β§ π£ β π β§ π€ β π΅)) β ((π’(.rβ(Scalarβπ))π£)( Β·π
βπ)π€) = (π’( Β·π
βπ)(π£(
Β·π βπ)π€))) |
148 | | simplll 774 |
. . . . 5
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β π) |
149 | | eqid 2733 |
. . . . . . . 8
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
150 | 11, 149 | ringidcl 19994 |
. . . . . . 7
β’
((Scalarβπ)
β Ring β (1rβ(Scalarβπ)) β π) |
151 | 17, 150 | syl 17 |
. . . . . 6
β’ (π β
(1rβ(Scalarβπ)) β π) |
152 | 151 | ad3antrrr 729 |
. . . . 5
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β
(1rβ(Scalarβπ)) β π) |
153 | | simplr 768 |
. . . . 5
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β π₯ β π) |
154 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17425 |
. . . . 5
β’ ((π β§
(1rβ(Scalarβπ)) β π β§ π₯ β π) β
((1rβ(Scalarβπ))( Β·π
βπ)(πΉβπ₯)) = (πΉβ((1rβ(Scalarβπ)) Β· π₯))) |
155 | 148, 152,
153, 154 | syl3anc 1372 |
. . . 4
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β
((1rβ(Scalarβπ))( Β·π
βπ)(πΉβπ₯)) = (πΉβ((1rβ(Scalarβπ)) Β· π₯))) |
156 | | simpr 486 |
. . . . 5
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β (πΉβπ₯) = π’) |
157 | 156 | oveq2d 7374 |
. . . 4
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β
((1rβ(Scalarβπ))( Β·π
βπ)(πΉβπ₯)) =
((1rβ(Scalarβπ))( Β·π
βπ)π’)) |
158 | 5 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β π β LMod) |
159 | 2, 8, 26, 149 | lmodvs1 20365 |
. . . . . . 7
β’ ((π β LMod β§ π₯ β π) β
((1rβ(Scalarβπ)) Β· π₯) = π₯) |
160 | 158, 153,
159 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β
((1rβ(Scalarβπ)) Β· π₯) = π₯) |
161 | 160 | fveq2d 6847 |
. . . . 5
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β (πΉβ((1rβ(Scalarβπ)) Β· π₯)) = (πΉβπ₯)) |
162 | 161, 156 | eqtrd 2773 |
. . . 4
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β (πΉβ((1rβ(Scalarβπ)) Β· π₯)) = π’) |
163 | 155, 157,
162 | 3eqtr3d 2781 |
. . 3
β’ ((((π β§ π’ β π΅) β§ π₯ β π) β§ (πΉβπ₯) = π’) β
((1rβ(Scalarβπ))( Β·π
βπ)π’) = π’) |
164 | | simpr 486 |
. . . . 5
β’ ((π β§ π’ β π΅) β π’ β π΅) |
165 | 82 | adantr 482 |
. . . . 5
β’ ((π β§ π’ β π΅) β ran πΉ = π΅) |
166 | 164, 165 | eleqtrrd 2837 |
. . . 4
β’ ((π β§ π’ β π΅) β π’ β ran πΉ) |
167 | | fvelrnb 6904 |
. . . . 5
β’ (πΉ Fn π β (π’ β ran πΉ β βπ₯ β π (πΉβπ₯) = π’)) |
168 | 167 | biimpa 478 |
. . . 4
β’ ((πΉ Fn π β§ π’ β ran πΉ) β βπ₯ β π (πΉβπ₯) = π’) |
169 | 79, 166, 168 | syl2an2r 684 |
. . 3
β’ ((π β§ π’ β π΅) β βπ₯ β π (πΉβπ₯) = π’) |
170 | 163, 169 | r19.29a 3156 |
. 2
β’ ((π β§ π’ β π΅) β
((1rβ(Scalarβπ))( Β·π
βπ)π’) = π’) |
171 | 6, 7, 9, 10, 12, 13, 14, 15, 17, 25, 35, 97, 130, 147, 170 | islmodd 20342 |
1
β’ (π β π β LMod) |