Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
β’ π΄ = (MEndoβπ) |
2 | 1 | mendbas 41554 |
. . 3
β’ (π LMHom π) = (Baseβπ΄) |
3 | 2 | a1i 11 |
. 2
β’ ((π β LMod β§ π β CRing) β (π LMHom π) = (Baseβπ΄)) |
4 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β
(+gβπ΄) =
(+gβπ΄)) |
5 | | mendassa.s |
. . . 4
β’ π = (Scalarβπ) |
6 | 1, 5 | mendsca 41559 |
. . 3
β’ π = (Scalarβπ΄) |
7 | 6 | a1i 11 |
. 2
β’ ((π β LMod β§ π β CRing) β π = (Scalarβπ΄)) |
8 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β (
Β·π βπ΄) = ( Β·π
βπ΄)) |
9 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β
(Baseβπ) =
(Baseβπ)) |
10 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β
(+gβπ) =
(+gβπ)) |
11 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β
(.rβπ) =
(.rβπ)) |
12 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β CRing) β
(1rβπ) =
(1rβπ)) |
13 | | crngring 19981 |
. . 3
β’ (π β CRing β π β Ring) |
14 | 13 | adantl 483 |
. 2
β’ ((π β LMod β§ π β CRing) β π β Ring) |
15 | 1 | mendring 41562 |
. . . 4
β’ (π β LMod β π΄ β Ring) |
16 | 15 | adantr 482 |
. . 3
β’ ((π β LMod β§ π β CRing) β π΄ β Ring) |
17 | | ringgrp 19974 |
. . 3
β’ (π΄ β Ring β π΄ β Grp) |
18 | 16, 17 | syl 17 |
. 2
β’ ((π β LMod β§ π β CRing) β π΄ β Grp) |
19 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
20 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
21 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
22 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ΄) = ( Β·π
βπ΄) |
23 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (π₯( Β·π
βπ΄)π¦) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
24 | 23 | 3adant1 1131 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (π₯( Β·π
βπ΄)π¦) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
25 | 21, 19, 5, 20 | lmhmvsca 20521 |
. . . 4
β’ ((π β CRing β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) β (π LMHom π)) |
26 | 25 | 3adant1l 1177 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) β (π LMHom π)) |
27 | 24, 26 | eqeltrd 2834 |
. 2
β’ (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (π₯( Β·π
βπ΄)π¦) β (π LMHom π)) |
28 | | simpr2 1196 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦ β (π LMHom π)) |
29 | | simpr3 1197 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π§ β (π LMHom π)) |
30 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
31 | | eqid 2733 |
. . . . . 6
β’
(+gβπ΄) = (+gβπ΄) |
32 | 1, 2, 30, 31 | mendplusg 41556 |
. . . . 5
β’ ((π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦(+gβπ΄)π§) = (π¦ βf
(+gβπ)π§)) |
33 | 28, 29, 32 | syl2anc 585 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦(+gβπ΄)π§) = (π¦ βf
(+gβπ)π§)) |
34 | 33 | oveq2d 7374 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦(+gβπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦ βf
(+gβπ)π§))) |
35 | | simpr1 1195 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π₯ β (Baseβπ)) |
36 | 18 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π΄ β Grp) |
37 | 2, 31 | grpcl 18761 |
. . . . 5
β’ ((π΄ β Grp β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π)) β (π¦(+gβπ΄)π§) β (π LMHom π)) |
38 | 36, 28, 29, 37 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π¦(+gβπ΄)π§) β (π LMHom π)) |
39 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . 4
β’ ((π₯ β (Baseβπ) β§ (π¦(+gβπ΄)π§) β (π LMHom π)) β (π₯( Β·π
βπ΄)(π¦(+gβπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦(+gβπ΄)π§))) |
40 | 35, 38, 39 | syl2anc 585 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)(π¦(+gβπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦(+gβπ΄)π§))) |
41 | 35, 28, 23 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π¦) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
42 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . . . 6
β’ ((π₯ β (Baseβπ) β§ π§ β (π LMHom π)) β (π₯( Β·π
βπ΄)π§) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§)) |
43 | 35, 29, 42 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π§) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§)) |
44 | 41, 43 | oveq12d 7376 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π¦) βf
(+gβπ)(π₯( Β·π
βπ΄)π§)) = ((((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) βf
(+gβπ)(((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§))) |
45 | 27 | 3adant3r3 1185 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π¦) β (π LMHom π)) |
46 | | eleq1w 2817 |
. . . . . . . . 9
β’ (π¦ = π§ β (π¦ β (π LMHom π) β π§ β (π LMHom π))) |
47 | 46 | 3anbi3d 1443 |
. . . . . . . 8
β’ (π¦ = π§ β (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β ((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π§ β (π LMHom π)))) |
48 | | oveq2 7366 |
. . . . . . . . 9
β’ (π¦ = π§ β (π₯( Β·π
βπ΄)π¦) = (π₯( Β·π
βπ΄)π§)) |
49 | 48 | eleq1d 2819 |
. . . . . . . 8
β’ (π¦ = π§ β ((π₯( Β·π
βπ΄)π¦) β (π LMHom π) β (π₯( Β·π
βπ΄)π§) β (π LMHom π))) |
50 | 47, 49 | imbi12d 345 |
. . . . . . 7
β’ (π¦ = π§ β ((((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π¦ β (π LMHom π)) β (π₯( Β·π
βπ΄)π¦) β (π LMHom π)) β (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π§ β (π LMHom π)) β (π₯( Β·π
βπ΄)π§) β (π LMHom π)))) |
51 | 50, 27 | chvarvv 2003 |
. . . . . 6
β’ (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π§ β (π LMHom π)) β (π₯( Β·π
βπ΄)π§) β (π LMHom π)) |
52 | 51 | 3adant3r2 1184 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π§) β (π LMHom π)) |
53 | 1, 2, 30, 31 | mendplusg 41556 |
. . . . 5
β’ (((π₯(
Β·π βπ΄)π¦) β (π LMHom π) β§ (π₯( Β·π
βπ΄)π§) β (π LMHom π)) β ((π₯( Β·π
βπ΄)π¦)(+gβπ΄)(π₯( Β·π
βπ΄)π§)) = ((π₯( Β·π
βπ΄)π¦) βf
(+gβπ)(π₯( Β·π
βπ΄)π§))) |
54 | 45, 52, 53 | syl2anc 585 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π¦)(+gβπ΄)(π₯( Β·π
βπ΄)π§)) = ((π₯( Β·π
βπ΄)π¦) βf
(+gβπ)(π₯( Β·π
βπ΄)π§))) |
55 | | fvexd 6858 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (Baseβπ) β V) |
56 | | fconst6g 6732 |
. . . . . 6
β’ (π₯ β (Baseβπ) β ((Baseβπ) Γ {π₯}):(Baseβπ)βΆ(Baseβπ)) |
57 | 35, 56 | syl 17 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {π₯}):(Baseβπ)βΆ(Baseβπ)) |
58 | 21, 21 | lmhmf 20510 |
. . . . . 6
β’ (π¦ β (π LMHom π) β π¦:(Baseβπ)βΆ(Baseβπ)) |
59 | 28, 58 | syl 17 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π¦:(Baseβπ)βΆ(Baseβπ)) |
60 | 21, 21 | lmhmf 20510 |
. . . . . 6
β’ (π§ β (π LMHom π) β π§:(Baseβπ)βΆ(Baseβπ)) |
61 | 29, 60 | syl 17 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π§:(Baseβπ)βΆ(Baseβπ)) |
62 | | simpll 766 |
. . . . . 6
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β π β LMod) |
63 | 21, 30, 5, 19, 20 | lmodvsdi 20360 |
. . . . . 6
β’ ((π β LMod β§ (π€ β (Baseβπ) β§ π£ β (Baseβπ) β§ π’ β (Baseβπ))) β (π€( Β·π
βπ)(π£(+gβπ)π’)) = ((π€( Β·π
βπ)π£)(+gβπ)(π€( Β·π
βπ)π’))) |
64 | 62, 63 | sylan 581 |
. . . . 5
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β§ (π€ β (Baseβπ) β§ π£ β (Baseβπ) β§ π’ β (Baseβπ))) β (π€( Β·π
βπ)(π£(+gβπ)π’)) = ((π€( Β·π
βπ)π£)(+gβπ)(π€( Β·π
βπ)π’))) |
65 | 55, 57, 59, 61, 64 | caofdi 7657 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦ βf
(+gβπ)π§)) = ((((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) βf
(+gβπ)(((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§))) |
66 | 44, 54, 65 | 3eqtr4d 2783 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π¦)(+gβπ΄)(π₯( Β·π
βπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦ βf
(+gβπ)π§))) |
67 | 34, 40, 66 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (π LMHom π) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)(π¦(+gβπ΄)π§)) = ((π₯( Β·π
βπ΄)π¦)(+gβπ΄)(π₯( Β·π
βπ΄)π§))) |
68 | | fvexd 6858 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (Baseβπ) β V) |
69 | | simpr3 1197 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π§ β (π LMHom π)) |
70 | 69, 60 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π§:(Baseβπ)βΆ(Baseβπ)) |
71 | | simpr1 1195 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π₯ β (Baseβπ)) |
72 | 71, 56 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {π₯}):(Baseβπ)βΆ(Baseβπ)) |
73 | | simpr2 1196 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π¦ β (Baseβπ)) |
74 | | fconst6g 6732 |
. . . . 5
β’ (π¦ β (Baseβπ) β ((Baseβπ) Γ {π¦}):(Baseβπ)βΆ(Baseβπ)) |
75 | 73, 74 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {π¦}):(Baseβπ)βΆ(Baseβπ)) |
76 | | simpll 766 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π β LMod) |
77 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
78 | 21, 30, 5, 19, 20, 77 | lmodvsdir 20361 |
. . . . 5
β’ ((π β LMod β§ (π€ β (Baseβπ) β§ π£ β (Baseβπ) β§ π’ β (Baseβπ))) β ((π€(+gβπ)π£)( Β·π
βπ)π’) = ((π€( Β·π
βπ)π’)(+gβπ)(π£( Β·π
βπ)π’))) |
79 | 76, 78 | sylan 581 |
. . . 4
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ (π€ β (Baseβπ) β§ π£ β (Baseβπ) β§ π’ β (Baseβπ))) β ((π€(+gβπ)π£)( Β·π
βπ)π’) = ((π€( Β·π
βπ)π’)(+gβπ)(π£( Β·π
βπ)π’))) |
80 | 68, 70, 72, 75, 79 | caofdir 7658 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((((Baseβπ) Γ {π₯}) βf
(+gβπ)((Baseβπ) Γ {π¦})) βf (
Β·π βπ)π§) = ((((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§) βf
(+gβπ)(((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§))) |
81 | 14 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π β Ring) |
82 | 20, 77 | ringacl 20004 |
. . . . . 6
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) β (Baseβπ)) |
83 | 81, 71, 73, 82 | syl3anc 1372 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯(+gβπ)π¦) β (Baseβπ)) |
84 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . . 5
β’ (((π₯(+gβπ)π¦) β (Baseβπ) β§ π§ β (π LMHom π)) β ((π₯(+gβπ)π¦)( Β·π
βπ΄)π§) = (((Baseβπ) Γ {(π₯(+gβπ)π¦)}) βf (
Β·π βπ)π§)) |
85 | 83, 69, 84 | syl2anc 585 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯(+gβπ)π¦)( Β·π
βπ΄)π§) = (((Baseβπ) Γ {(π₯(+gβπ)π¦)}) βf (
Β·π βπ)π§)) |
86 | 68, 71, 73 | ofc12 7646 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {π₯}) βf
(+gβπ)((Baseβπ) Γ {π¦})) = ((Baseβπ) Γ {(π₯(+gβπ)π¦)})) |
87 | 86 | oveq1d 7373 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((((Baseβπ) Γ {π₯}) βf
(+gβπ)((Baseβπ) Γ {π¦})) βf (
Β·π βπ)π§) = (((Baseβπ) Γ {(π₯(+gβπ)π¦)}) βf (
Β·π βπ)π§)) |
88 | 85, 87 | eqtr4d 2776 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯(+gβπ)π¦)( Β·π
βπ΄)π§) = ((((Baseβπ) Γ {π₯}) βf
(+gβπ)((Baseβπ) Γ {π¦})) βf (
Β·π βπ)π§)) |
89 | 51 | 3adant3r2 1184 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π§) β (π LMHom π)) |
90 | | eleq1w 2817 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯ β (Baseβπ) β π¦ β (Baseβπ))) |
91 | 90 | 3anbi2d 1442 |
. . . . . . . 8
β’ (π₯ = π¦ β (((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π§ β (π LMHom π)) β ((π β LMod β§ π β CRing) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π)))) |
92 | | oveq1 7365 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π₯( Β·π
βπ΄)π§) = (π¦( Β·π
βπ΄)π§)) |
93 | 92 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π₯( Β·π
βπ΄)π§) β (π LMHom π) β (π¦( Β·π
βπ΄)π§) β (π LMHom π))) |
94 | 91, 93 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π¦ β ((((π β LMod β§ π β CRing) β§ π₯ β (Baseβπ) β§ π§ β (π LMHom π)) β (π₯( Β·π
βπ΄)π§) β (π LMHom π)) β (((π β LMod β§ π β CRing) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π)) β (π¦( Β·π
βπ΄)π§) β (π LMHom π)))) |
95 | 94, 51 | chvarvv 2003 |
. . . . . 6
β’ (((π β LMod β§ π β CRing) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π)) β (π¦( Β·π
βπ΄)π§) β (π LMHom π)) |
96 | 95 | 3adant3r1 1183 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π¦( Β·π
βπ΄)π§) β (π LMHom π)) |
97 | 1, 2, 30, 31 | mendplusg 41556 |
. . . . 5
β’ (((π₯(
Β·π βπ΄)π§) β (π LMHom π) β§ (π¦( Β·π
βπ΄)π§) β (π LMHom π)) β ((π₯( Β·π
βπ΄)π§)(+gβπ΄)(π¦( Β·π
βπ΄)π§)) = ((π₯( Β·π
βπ΄)π§) βf
(+gβπ)(π¦( Β·π
βπ΄)π§))) |
98 | 89, 96, 97 | syl2anc 585 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π§)(+gβπ΄)(π¦( Β·π
βπ΄)π§)) = ((π₯( Β·π
βπ΄)π§) βf
(+gβπ)(π¦( Β·π
βπ΄)π§))) |
99 | 71, 69, 42 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)π§) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§)) |
100 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . . . 6
β’ ((π¦ β (Baseβπ) β§ π§ β (π LMHom π)) β (π¦( Β·π
βπ΄)π§) = (((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§)) |
101 | 73, 69, 100 | syl2anc 585 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π¦( Β·π
βπ΄)π§) = (((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§)) |
102 | 99, 101 | oveq12d 7376 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π§) βf
(+gβπ)(π¦( Β·π
βπ΄)π§)) = ((((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§) βf
(+gβπ)(((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§))) |
103 | 98, 102 | eqtrd 2773 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯( Β·π
βπ΄)π§)(+gβπ΄)(π¦( Β·π
βπ΄)π§)) = ((((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π§) βf
(+gβπ)(((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§))) |
104 | 80, 88, 103 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯(+gβπ)π¦)( Β·π
βπ΄)π§) = ((π₯( Β·π
βπ΄)π§)(+gβπ΄)(π¦( Β·π
βπ΄)π§))) |
105 | | ovexd 7393 |
. . . 4
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β (π₯(.rβπ)π¦) β V) |
106 | 70 | ffvelcdmda 7036 |
. . . 4
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β (π§βπ) β (Baseβπ)) |
107 | | fconstmpt 5695 |
. . . . 5
β’
((Baseβπ)
Γ {(π₯(.rβπ)π¦)}) = (π β (Baseβπ) β¦ (π₯(.rβπ)π¦)) |
108 | 107 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {(π₯(.rβπ)π¦)}) = (π β (Baseβπ) β¦ (π₯(.rβπ)π¦))) |
109 | 70 | feqmptd 6911 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β π§ = (π β (Baseβπ) β¦ (π§βπ))) |
110 | 68, 105, 106, 108, 109 | offval2 7638 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {(π₯(.rβπ)π¦)}) βf (
Β·π βπ)π§) = (π β (Baseβπ) β¦ ((π₯(.rβπ)π¦)( Β·π
βπ)(π§βπ)))) |
111 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
112 | 20, 111 | ringcl 19986 |
. . . . 5
β’ ((π β Ring β§ π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(.rβπ)π¦) β (Baseβπ)) |
113 | 81, 71, 73, 112 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯(.rβπ)π¦) β (Baseβπ)) |
114 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . 4
β’ (((π₯(.rβπ)π¦) β (Baseβπ) β§ π§ β (π LMHom π)) β ((π₯(.rβπ)π¦)( Β·π
βπ΄)π§) = (((Baseβπ) Γ {(π₯(.rβπ)π¦)}) βf (
Β·π βπ)π§)) |
115 | 113, 69, 114 | syl2anc 585 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯(.rβπ)π¦)( Β·π
βπ΄)π§) = (((Baseβπ) Γ {(π₯(.rβπ)π¦)}) βf (
Β·π βπ)π§)) |
116 | 71 | adantr 482 |
. . . . 5
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β π₯ β (Baseβπ)) |
117 | | ovexd 7393 |
. . . . 5
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β (π¦( Β·π
βπ)(π§βπ)) β V) |
118 | | fconstmpt 5695 |
. . . . . 6
β’
((Baseβπ)
Γ {π₯}) = (π β (Baseβπ) β¦ π₯) |
119 | 118 | a1i 11 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {π₯}) = (π β (Baseβπ) β¦ π₯)) |
120 | | simplr2 1217 |
. . . . . . 7
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β π¦ β (Baseβπ)) |
121 | | fconstmpt 5695 |
. . . . . . . 8
β’
((Baseβπ)
Γ {π¦}) = (π β (Baseβπ) β¦ π¦) |
122 | 121 | a1i 11 |
. . . . . . 7
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((Baseβπ) Γ {π¦}) = (π β (Baseβπ) β¦ π¦)) |
123 | 68, 120, 106, 122, 109 | offval2 7638 |
. . . . . 6
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {π¦}) βf (
Β·π βπ)π§) = (π β (Baseβπ) β¦ (π¦( Β·π
βπ)(π§βπ)))) |
124 | 101, 123 | eqtrd 2773 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π¦( Β·π
βπ΄)π§) = (π β (Baseβπ) β¦ (π¦( Β·π
βπ)(π§βπ)))) |
125 | 68, 116, 117, 119, 124 | offval2 7638 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦( Β·π
βπ΄)π§)) = (π β (Baseβπ) β¦ (π₯( Β·π
βπ)(π¦(
Β·π βπ)(π§βπ))))) |
126 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . . 5
β’ ((π₯ β (Baseβπ) β§ (π¦( Β·π
βπ΄)π§) β (π LMHom π)) β (π₯( Β·π
βπ΄)(π¦(
Β·π βπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦( Β·π
βπ΄)π§))) |
127 | 71, 96, 126 | syl2anc 585 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)(π¦(
Β·π βπ΄)π§)) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)(π¦( Β·π
βπ΄)π§))) |
128 | 76 | adantr 482 |
. . . . . 6
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β π β LMod) |
129 | 21, 5, 19, 20, 111 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ (π§βπ) β (Baseβπ))) β ((π₯(.rβπ)π¦)( Β·π
βπ)(π§βπ)) = (π₯( Β·π
βπ)(π¦(
Β·π βπ)(π§βπ)))) |
130 | 128, 116,
120, 106, 129 | syl13anc 1373 |
. . . . 5
β’ ((((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β§ π β (Baseβπ)) β ((π₯(.rβπ)π¦)( Β·π
βπ)(π§βπ)) = (π₯( Β·π
βπ)(π¦(
Β·π βπ)(π§βπ)))) |
131 | 130 | mpteq2dva 5206 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π β (Baseβπ) β¦ ((π₯(.rβπ)π¦)( Β·π
βπ)(π§βπ))) = (π β (Baseβπ) β¦ (π₯( Β·π
βπ)(π¦(
Β·π βπ)(π§βπ))))) |
132 | 125, 127,
131 | 3eqtr4d 2783 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β (π₯( Β·π
βπ΄)(π¦(
Β·π βπ΄)π§)) = (π β (Baseβπ) β¦ ((π₯(.rβπ)π¦)( Β·π
βπ)(π§βπ)))) |
133 | 110, 115,
132 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π β CRing) β§ (π₯ β (Baseβπ) β§ π¦ β (Baseβπ) β§ π§ β (π LMHom π))) β ((π₯(.rβπ)π¦)( Β·π
βπ΄)π§) = (π₯( Β·π
βπ΄)(π¦(
Β·π βπ΄)π§))) |
134 | 14 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β π β Ring) |
135 | | eqid 2733 |
. . . . . 6
β’
(1rβπ) = (1rβπ) |
136 | 20, 135 | ringidcl 19994 |
. . . . 5
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
137 | 134, 136 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β (1rβπ) β (Baseβπ)) |
138 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 41561 |
. . . 4
β’
(((1rβπ) β (Baseβπ) β§ π₯ β (π LMHom π)) β ((1rβπ)(
Β·π βπ΄)π₯) = (((Baseβπ) Γ {(1rβπ)}) βf (
Β·π βπ)π₯)) |
139 | 137, 138 | sylancom 589 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β ((1rβπ)(
Β·π βπ΄)π₯) = (((Baseβπ) Γ {(1rβπ)}) βf (
Β·π βπ)π₯)) |
140 | | fvexd 6858 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β (Baseβπ) β V) |
141 | 21, 21 | lmhmf 20510 |
. . . . 5
β’ (π₯ β (π LMHom π) β π₯:(Baseβπ)βΆ(Baseβπ)) |
142 | 141 | adantl 483 |
. . . 4
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β π₯:(Baseβπ)βΆ(Baseβπ)) |
143 | | simpll 766 |
. . . . 5
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β π β LMod) |
144 | 21, 5, 19, 135 | lmodvs1 20365 |
. . . . 5
β’ ((π β LMod β§ π¦ β (Baseβπ)) β
((1rβπ)(
Β·π βπ)π¦) = π¦) |
145 | 143, 144 | sylan 581 |
. . . 4
β’ ((((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β§ π¦ β (Baseβπ)) β ((1rβπ)(
Β·π βπ)π¦) = π¦) |
146 | 140, 142,
137, 145 | caofid0l 7649 |
. . 3
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β (((Baseβπ) Γ {(1rβπ)}) βf (
Β·π βπ)π₯) = π₯) |
147 | 139, 146 | eqtrd 2773 |
. 2
β’ (((π β LMod β§ π β CRing) β§ π₯ β (π LMHom π)) β ((1rβπ)(
Β·π βπ΄)π₯) = π₯) |
148 | 3, 4, 7, 8, 9, 10,
11, 12, 14, 18, 27, 67, 104, 133, 147 | islmodd 20342 |
1
β’ ((π β LMod β§ π β CRing) β π΄ β LMod) |