Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
⊢ 𝐴 = (MEndo‘𝑀) |
2 | 1 | mendbas 36773 |
. . 3
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (𝑀 LMHom 𝑀) = (Base‘𝐴)) |
4 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(+g‘𝐴) =
(+g‘𝐴)) |
5 | | mendassa.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑀) |
6 | 1, 5 | mendsca 36778 |
. . 3
⊢ 𝑆 = (Scalar‘𝐴) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 = (Scalar‘𝐴)) |
8 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
9 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(Base‘𝑆) =
(Base‘𝑆)) |
10 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(+g‘𝑆) =
(+g‘𝑆)) |
11 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(.r‘𝑆) =
(.r‘𝑆)) |
12 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(1r‘𝑆) =
(1r‘𝑆)) |
13 | | crngring 18381 |
. . 3
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
14 | 13 | adantl 481 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 ∈ Ring) |
15 | 1 | mendring 36781 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |
16 | 15 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Ring) |
17 | | ringgrp 18375 |
. . 3
⊢ (𝐴 ∈ Ring → 𝐴 ∈ Grp) |
18 | 16, 17 | syl 17 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Grp) |
19 | | eqid 2610 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
20 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
21 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
22 | | eqid 2610 |
. . . . 5
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
23 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
24 | 23 | 3adant1 1072 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
25 | 21, 19, 5, 20 | lmhmvsca 18866 |
. . . 4
⊢ ((𝑆 ∈ CRing ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
26 | 25 | 3adant1l 1310 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
27 | 24, 26 | eqeltrd 2688 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
28 | | simpr2 1061 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
29 | | simpr3 1062 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
30 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
31 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝐴) = (+g‘𝐴) |
32 | 1, 2, 30, 31 | mendplusg 36775 |
. . . . 5
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘𝑓
(+g‘𝑀)𝑧)) |
33 | 28, 29, 32 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘𝑓
(+g‘𝑀)𝑧)) |
34 | 33 | oveq2d 6565 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦 ∘𝑓
(+g‘𝑀)𝑧))) |
35 | | simpr1 1060 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
36 | 18 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ Grp) |
37 | 2, 31 | grpcl 17253 |
. . . . 5
⊢ ((𝐴 ∈ Grp ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
38 | 36, 28, 29, 37 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
39 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧))) |
40 | 35, 38, 39 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧))) |
41 | 35, 28, 23 | syl2anc 691 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
42 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
43 | 35, 29, 42 | syl2anc 691 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
44 | 41, 43 | oveq12d 6567 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘𝑓
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) ∘𝑓
(+g‘𝑀)(((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧))) |
45 | 27 | 3adant3r3 1268 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
46 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑀 LMHom 𝑀) ↔ 𝑧 ∈ (𝑀 LMHom 𝑀))) |
47 | 46 | 3anbi3d 1397 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) ↔ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)))) |
48 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑥( ·𝑠
‘𝐴)𝑦) = (𝑥( ·𝑠
‘𝐴)𝑧)) |
49 | 48 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ↔ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀))) |
50 | 47, 49 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) ↔ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)))) |
51 | 50, 27 | chvarv 2251 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
52 | 51 | 3adant3r2 1267 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
53 | 1, 2, 30, 31 | mendplusg 36775 |
. . . . 5
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘𝑓
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧))) |
54 | 45, 52, 53 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘𝑓
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧))) |
55 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑀)
∈ V |
56 | 55 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
57 | | fconst6g 6007 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑆) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
58 | 35, 57 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
59 | 21, 21 | lmhmf 18855 |
. . . . . 6
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
60 | 28, 59 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
61 | 21, 21 | lmhmf 18855 |
. . . . . 6
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
62 | 29, 61 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
63 | | simpll 786 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑀 ∈ LMod) |
64 | 21, 30, 5, 19, 20 | lmodvsdi 18709 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑀) ∧ 𝑢 ∈ (Base‘𝑀))) → (𝑤( ·𝑠
‘𝑀)(𝑣(+g‘𝑀)𝑢)) = ((𝑤( ·𝑠
‘𝑀)𝑣)(+g‘𝑀)(𝑤( ·𝑠
‘𝑀)𝑢))) |
65 | 63, 64 | sylan 487 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑀) ∧ 𝑢 ∈ (Base‘𝑀))) → (𝑤( ·𝑠
‘𝑀)(𝑣(+g‘𝑀)𝑢)) = ((𝑤( ·𝑠
‘𝑀)𝑣)(+g‘𝑀)(𝑤( ·𝑠
‘𝑀)𝑢))) |
66 | 56, 58, 60, 62, 65 | caofdi 6831 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦 ∘𝑓
(+g‘𝑀)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) ∘𝑓
(+g‘𝑀)(((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧))) |
67 | 44, 54, 66 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦 ∘𝑓
(+g‘𝑀)𝑧))) |
68 | 34, 40, 67 | 3eqtr4d 2654 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧))) |
69 | 55 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
70 | | simpr3 1062 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
71 | 70, 61 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
72 | | simpr1 1060 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
73 | 72, 57 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
74 | | simpr2 1061 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (Base‘𝑆)) |
75 | | fconst6g 6007 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝑆) → ((Base‘𝑀) × {𝑦}):(Base‘𝑀)⟶(Base‘𝑆)) |
76 | 74, 75 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑦}):(Base‘𝑀)⟶(Base‘𝑆)) |
77 | | simpll 786 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑀 ∈ LMod) |
78 | | eqid 2610 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
79 | 21, 30, 5, 19, 20, 78 | lmodvsdir 18710 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑆) ∧ 𝑢 ∈ (Base‘𝑀))) → ((𝑤(+g‘𝑆)𝑣)( ·𝑠
‘𝑀)𝑢) = ((𝑤( ·𝑠
‘𝑀)𝑢)(+g‘𝑀)(𝑣( ·𝑠
‘𝑀)𝑢))) |
80 | 77, 79 | sylan 487 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑆) ∧ 𝑢 ∈ (Base‘𝑀))) → ((𝑤(+g‘𝑆)𝑣)( ·𝑠
‘𝑀)𝑢) = ((𝑤( ·𝑠
‘𝑀)𝑢)(+g‘𝑀)(𝑣( ·𝑠
‘𝑀)𝑢))) |
81 | 69, 71, 73, 76, 80 | caofdir 6832 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((((Base‘𝑀) × {𝑥}) ∘𝑓
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) = ((((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) ∘𝑓
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧))) |
82 | 14 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑆 ∈ Ring) |
83 | 20, 78 | ringacl 18401 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
84 | 82, 72, 74, 83 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
85 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . . 5
⊢ (((𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
86 | 84, 70, 85 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
87 | 69, 72, 74 | ofc12 6820 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓
(+g‘𝑆)((Base‘𝑀) × {𝑦})) = ((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)})) |
88 | 87 | oveq1d 6564 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((((Base‘𝑀) × {𝑥}) ∘𝑓
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
89 | 86, 88 | eqtr4d 2647 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = ((((Base‘𝑀) × {𝑥}) ∘𝑓
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
90 | 51 | 3adant3r2 1267 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
91 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (Base‘𝑆) ↔ 𝑦 ∈ (Base‘𝑆))) |
92 | 91 | 3anbi2d 1396 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) ↔ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)))) |
93 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥( ·𝑠
‘𝐴)𝑧) = (𝑦( ·𝑠
‘𝐴)𝑧)) |
94 | 93 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀) ↔ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀))) |
95 | 92, 94 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) ↔ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)))) |
96 | 95, 51 | chvarv 2251 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
97 | 96 | 3adant3r1 1266 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
98 | 1, 2, 30, 31 | mendplusg 36775 |
. . . . 5
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀) ∧ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑧) ∘𝑓
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
99 | 90, 97, 98 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑧) ∘𝑓
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
100 | 72, 70, 42 | syl2anc 691 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
101 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . . . 6
⊢ ((𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
102 | 74, 70, 101 | syl2anc 691 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
103 | 100, 102 | oveq12d 6567 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧) ∘𝑓
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) ∘𝑓
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧))) |
104 | 99, 103 | eqtrd 2644 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) ∘𝑓
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧))) |
105 | 81, 89, 104 | 3eqtr4d 2654 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧))) |
106 | | ovex 6577 |
. . . . 5
⊢ (𝑥(.r‘𝑆)𝑦) ∈ V |
107 | 106 | a1i 11 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑥(.r‘𝑆)𝑦) ∈ V) |
108 | 71 | ffvelrnda 6267 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑧‘𝑘) ∈ (Base‘𝑀)) |
109 | | fconstmpt 5085 |
. . . . 5
⊢
((Base‘𝑀)
× {(𝑥(.r‘𝑆)𝑦)}) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥(.r‘𝑆)𝑦)) |
110 | 109 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥(.r‘𝑆)𝑦))) |
111 | 71 | feqmptd 6159 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 = (𝑘 ∈ (Base‘𝑀) ↦ (𝑧‘𝑘))) |
112 | 69, 107, 108, 110, 111 | offval2 6812 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
113 | | eqid 2610 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
114 | 20, 113 | ringcl 18384 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆)) |
115 | 82, 72, 74, 114 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆)) |
116 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . 4
⊢ (((𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
117 | 115, 70, 116 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
118 | 72 | adantr 480 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
119 | | ovex 6577 |
. . . . . 6
⊢ (𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘)) ∈ V |
120 | 119 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)) ∈ V) |
121 | | fconstmpt 5085 |
. . . . . 6
⊢
((Base‘𝑀)
× {𝑥}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑥) |
122 | 121 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑥)) |
123 | | simplr2 1097 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑦 ∈ (Base‘𝑆)) |
124 | | fconstmpt 5085 |
. . . . . . . 8
⊢
((Base‘𝑀)
× {𝑦}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑦) |
125 | 124 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑦}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑦)) |
126 | 69, 123, 108, 125, 111 | offval2 6812 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑦}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
127 | 102, 126 | eqtrd 2644 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
128 | 69, 118, 120, 122, 127 | offval2 6812 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧)) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘))))) |
129 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
130 | 72, 97, 129 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
131 | 77 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑀 ∈ LMod) |
132 | 21, 5, 19, 20, 113 | lmodvsass 18711 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ (𝑧‘𝑘) ∈ (Base‘𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)) = (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘)))) |
133 | 131, 118,
123, 108, 132 | syl13anc 1320 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)) = (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘)))) |
134 | 133 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘))) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘))))) |
135 | 128, 130,
134 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
136 | 112, 117,
135 | 3eqtr4d 2654 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧))) |
137 | 14 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑆 ∈ Ring) |
138 | | eqid 2610 |
. . . . . 6
⊢
(1r‘𝑆) = (1r‘𝑆) |
139 | 20, 138 | ringidcl 18391 |
. . . . 5
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
140 | 137, 139 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (1r‘𝑆) ∈ (Base‘𝑆)) |
141 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 36780 |
. . . 4
⊢
(((1r‘𝑆) ∈ (Base‘𝑆) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = (((Base‘𝑀) × {(1r‘𝑆)}) ∘𝑓
( ·𝑠 ‘𝑀)𝑥)) |
142 | 140, 141 | sylancom 698 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = (((Base‘𝑀) × {(1r‘𝑆)}) ∘𝑓
( ·𝑠 ‘𝑀)𝑥)) |
143 | 55 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (Base‘𝑀) ∈ V) |
144 | 21, 21 | lmhmf 18855 |
. . . . 5
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
145 | 144 | adantl 481 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
146 | | simpll 786 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑀 ∈ LMod) |
147 | 21, 5, 19, 138 | lmodvs1 18714 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑀)) →
((1r‘𝑆)(
·𝑠 ‘𝑀)𝑦) = 𝑦) |
148 | 146, 147 | sylan 487 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝑀)𝑦) = 𝑦) |
149 | 143, 145,
140, 148 | caofid0l 6823 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(1r‘𝑆)}) ∘𝑓
( ·𝑠 ‘𝑀)𝑥) = 𝑥) |
150 | 142, 149 | eqtrd 2644 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = 𝑥) |
151 | 3, 4, 7, 8, 9, 10,
11, 12, 14, 18, 27, 68, 105, 136, 150 | islmodd 18692 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) |