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 17017 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑁)) |
7 | | eqidd 2738 |
. 2
⊢ (𝜑 → (+g‘𝑁) = (+g‘𝑁)) |
8 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
9 | 1, 3, 4, 5, 8 | imassca 17024 |
. 2
⊢ (𝜑 → (Scalar‘𝑀) = (Scalar‘𝑁)) |
10 | | eqidd 2738 |
. 2
⊢ (𝜑 → (
·𝑠 ‘𝑁) = ( ·𝑠
‘𝑁)) |
11 | | imaslmod.k |
. . 3
⊢ 𝑆 =
(Base‘(Scalar‘𝑀)) |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → 𝑆 = (Base‘(Scalar‘𝑀))) |
13 | | eqidd 2738 |
. 2
⊢ (𝜑 →
(+g‘(Scalar‘𝑀)) =
(+g‘(Scalar‘𝑀))) |
14 | | eqidd 2738 |
. 2
⊢ (𝜑 →
(.r‘(Scalar‘𝑀)) =
(.r‘(Scalar‘𝑀))) |
15 | | eqidd 2738 |
. 2
⊢ (𝜑 →
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀))) |
16 | 8 | lmodring 19907 |
. . 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 19906 |
. . . . 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 18479 |
. . 3
⊢ (𝜑 → (𝑁 ∈ Grp ∧ (𝐹‘ 0 ) =
(0g‘𝑁))) |
25 | 24 | simpld 498 |
. 2
⊢ (𝜑 → 𝑁 ∈ Grp) |
26 | | imaslmod.t |
. . . 4
⊢ · = (
·𝑠 ‘𝑀) |
27 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑁) = ( ·𝑠
‘𝑁) |
28 | | imaslmod.e2 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏)))) |
29 | 5 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉)) → 𝑀 ∈ LMod) |
30 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉)) → 𝑘 ∈ 𝑆) |
31 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉)) → 𝑏 ∈ 𝑉) |
32 | 2, 8, 26, 11 | lmodvscl 19916 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉) → (𝑘 · 𝑏) ∈ 𝑉) |
33 | 29, 30, 31, 32 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉)) → (𝑘 · 𝑏) ∈ 𝑉) |
34 | 1, 3, 4, 5, 8, 11,
26, 27, 28, 33 | imasvscaf 17044 |
. . 3
⊢ (𝜑 → (
·𝑠 ‘𝑁):(𝑆 × 𝐵)⟶𝐵) |
35 | 34 | fovcld 30694 |
. 2
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵) → (𝑢( ·𝑠
‘𝑁)𝑣) ∈ 𝐵) |
36 | | simp-5l 785 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝜑) |
37 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) |
38 | 37 | simp1d 1144 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑢 ∈ 𝑆) |
39 | 38 | ad2antrr 726 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝑢 ∈ 𝑆) |
40 | 36, 22 | syl 17 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝑀 ∈ Grp) |
41 | | simplr 769 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝑦 ∈ 𝑉) |
42 | | simp-4r 784 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝑧 ∈ 𝑉) |
43 | 2, 18 | grpcl 18373 |
. . . . . . . 8
⊢ ((𝑀 ∈ Grp ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑦 + 𝑧) ∈ 𝑉) |
44 | 40, 41, 42, 43 | syl3anc 1373 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑦 + 𝑧) ∈ 𝑉) |
45 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ (𝑦 + 𝑧) ∈ 𝑉) → (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑢 · (𝑦 + 𝑧)))) |
46 | 36, 39, 44, 45 | syl3anc 1373 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑢 · (𝑦 + 𝑧)))) |
47 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑁) = (+g‘𝑁) |
48 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17037 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+g‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧))) |
49 | 36, 41, 42, 48 | syl3anc 1373 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → ((𝐹‘𝑦)(+g‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧))) |
50 | | simpr 488 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘𝑦) = 𝑣) |
51 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘𝑧) = 𝑤) |
52 | 50, 51 | oveq12d 7231 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → ((𝐹‘𝑦)(+g‘𝑁)(𝐹‘𝑧)) = (𝑣(+g‘𝑁)𝑤)) |
53 | 49, 52 | eqtr3d 2779 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘(𝑦 + 𝑧)) = (𝑣(+g‘𝑁)𝑤)) |
54 | 53 | oveq2d 7229 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑦 + 𝑧))) = (𝑢( ·𝑠
‘𝑁)(𝑣(+g‘𝑁)𝑤))) |
55 | 36, 5 | syl 17 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → 𝑀 ∈ LMod) |
56 | 2, 18, 8, 26, 11 | lmodvsdi 19922 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑢 · (𝑦 + 𝑧)) = ((𝑢 · 𝑦) + (𝑢 · 𝑧))) |
57 | 55, 39, 41, 42, 56 | syl13anc 1374 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢 · (𝑦 + 𝑧)) = ((𝑢 · 𝑦) + (𝑢 · 𝑧))) |
58 | 57 | fveq2d 6721 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘(𝑢 · (𝑦 + 𝑧))) = (𝐹‘((𝑢 · 𝑦) + (𝑢 · 𝑧)))) |
59 | 46, 54, 58 | 3eqtr3d 2785 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝑣(+g‘𝑁)𝑤)) = (𝐹‘((𝑢 · 𝑦) + (𝑢 · 𝑧)))) |
60 | 2, 8, 26, 11 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉) → (𝑢 · 𝑦) ∈ 𝑉) |
61 | 55, 39, 41, 60 | syl3anc 1373 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢 · 𝑦) ∈ 𝑉) |
62 | 2, 8, 26, 11 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → (𝑢 · 𝑧) ∈ 𝑉) |
63 | 55, 39, 42, 62 | syl3anc 1373 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢 · 𝑧) ∈ 𝑉) |
64 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17037 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 · 𝑦) ∈ 𝑉 ∧ (𝑢 · 𝑧) ∈ 𝑉) → ((𝐹‘(𝑢 · 𝑦))(+g‘𝑁)(𝐹‘(𝑢 · 𝑧))) = (𝐹‘((𝑢 · 𝑦) + (𝑢 · 𝑧)))) |
65 | 36, 61, 63, 64 | syl3anc 1373 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → ((𝐹‘(𝑢 · 𝑦))(+g‘𝑁)(𝐹‘(𝑢 · 𝑧))) = (𝐹‘((𝑢 · 𝑦) + (𝑢 · 𝑧)))) |
66 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑦)) = (𝐹‘(𝑢 · 𝑦))) |
67 | 36, 39, 41, 66 | syl3anc 1373 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑦)) = (𝐹‘(𝑢 · 𝑦))) |
68 | 50 | oveq2d 7229 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑦)) = (𝑢( ·𝑠
‘𝑁)𝑣)) |
69 | 67, 68 | eqtr3d 2779 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘(𝑢 · 𝑦)) = (𝑢( ·𝑠
‘𝑁)𝑣)) |
70 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑢 · 𝑧))) |
71 | 36, 39, 42, 70 | syl3anc 1373 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑢 · 𝑧))) |
72 | 51 | oveq2d 7229 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝑢( ·𝑠
‘𝑁)𝑤)) |
73 | 71, 72 | eqtr3d 2779 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝐹‘(𝑢 · 𝑧)) = (𝑢( ·𝑠
‘𝑁)𝑤)) |
74 | 69, 73 | oveq12d 7231 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → ((𝐹‘(𝑢 · 𝑦))(+g‘𝑁)(𝐹‘(𝑢 · 𝑧))) = ((𝑢( ·𝑠
‘𝑁)𝑣)(+g‘𝑁)(𝑢( ·𝑠
‘𝑁)𝑤))) |
75 | 59, 65, 74 | 3eqtr2d 2783 |
. . . 4
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) ∧ 𝑦 ∈ 𝑉) ∧ (𝐹‘𝑦) = 𝑣) → (𝑢( ·𝑠
‘𝑁)(𝑣(+g‘𝑁)𝑤)) = ((𝑢( ·𝑠
‘𝑁)𝑣)(+g‘𝑁)(𝑢( ·𝑠
‘𝑁)𝑤))) |
76 | | simplll 775 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝜑) |
77 | 37 | simp2d 1145 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑣 ∈ 𝐵) |
78 | | fofn 6635 |
. . . . . . 7
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
79 | 4, 78 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn 𝑉) |
80 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵) |
81 | | forn 6636 |
. . . . . . . . 9
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
82 | 4, 81 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 = 𝐵) |
83 | 82 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → ran 𝐹 = 𝐵) |
84 | 80, 83 | eleqtrrd 2841 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ ran 𝐹) |
85 | | fvelrnb 6773 |
. . . . . . 7
⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣)) |
86 | 85 | biimpa 480 |
. . . . . 6
⊢ ((𝐹 Fn 𝑉 ∧ 𝑣 ∈ ran 𝐹) → ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣) |
87 | 79, 84, 86 | syl2an2r 685 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣) |
88 | 76, 77, 87 | syl2anc 587 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣) |
89 | 75, 88 | r19.29a 3208 |
. . 3
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝑣(+g‘𝑁)𝑤)) = ((𝑢( ·𝑠
‘𝑁)𝑣)(+g‘𝑁)(𝑢( ·𝑠
‘𝑁)𝑤))) |
90 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝐵) |
91 | 82 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ran 𝐹 = 𝐵) |
92 | 90, 91 | eleqtrrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ ran 𝐹) |
93 | | fvelrnb 6773 |
. . . . . 6
⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)) |
94 | 93 | biimpa 480 |
. . . . 5
⊢ ((𝐹 Fn 𝑉 ∧ 𝑤 ∈ ran 𝐹) → ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤) |
95 | 79, 92, 94 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤) |
96 | 95 | 3ad2antr3 1192 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤) |
97 | 89, 96 | r19.29a 3208 |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢( ·𝑠
‘𝑁)(𝑣(+g‘𝑁)𝑤)) = ((𝑢( ·𝑠
‘𝑁)𝑣)(+g‘𝑁)(𝑢( ·𝑠
‘𝑁)𝑤))) |
98 | | simplll 775 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝜑) |
99 | 5 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑀 ∈ LMod) |
100 | | simpllr 776 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) |
101 | 100 | simp1d 1144 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑢 ∈ 𝑆) |
102 | 100 | simp2d 1145 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑣 ∈ 𝑆) |
103 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(Scalar‘𝑀)) =
(+g‘(Scalar‘𝑀)) |
104 | 8, 11, 103 | lmodacl 19910 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢(+g‘(Scalar‘𝑀))𝑣) ∈ 𝑆) |
105 | 99, 101, 102, 104 | syl3anc 1373 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢(+g‘(Scalar‘𝑀))𝑣) ∈ 𝑆) |
106 | | simplr 769 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → 𝑧 ∈ 𝑉) |
107 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢(+g‘(Scalar‘𝑀))𝑣) ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧))) |
108 | 98, 105, 106, 107 | syl3anc 1373 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧))) |
109 | | simpr 488 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤) |
110 | 109 | oveq2d 7229 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤)) |
111 | 2, 18, 8, 26, 11, 103 | lmodvsdir 19923 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉)) → ((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧) = ((𝑢 · 𝑧) + (𝑣 · 𝑧))) |
112 | 99, 101, 102, 106, 111 | syl13anc 1374 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧) = ((𝑢 · 𝑧) + (𝑣 · 𝑧))) |
113 | 112 | fveq2d 6721 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧)) = (𝐹‘((𝑢 · 𝑧) + (𝑣 · 𝑧)))) |
114 | 99, 101, 106, 62 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢 · 𝑧) ∈ 𝑉) |
115 | 2, 8, 26, 11 | lmodvscl 19916 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → (𝑣 · 𝑧) ∈ 𝑉) |
116 | 99, 102, 106, 115 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑣 · 𝑧) ∈ 𝑉) |
117 | 4, 20, 1, 3, 5, 18,
47 | imasaddval 17037 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 · 𝑧) ∈ 𝑉 ∧ (𝑣 · 𝑧) ∈ 𝑉) → ((𝐹‘(𝑢 · 𝑧))(+g‘𝑁)(𝐹‘(𝑣 · 𝑧))) = (𝐹‘((𝑢 · 𝑧) + (𝑣 · 𝑧)))) |
118 | 98, 114, 116, 117 | syl3anc 1373 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘(𝑢 · 𝑧))(+g‘𝑁)(𝐹‘(𝑣 · 𝑧))) = (𝐹‘((𝑢 · 𝑧) + (𝑣 · 𝑧)))) |
119 | 98, 101, 106, 70 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑢 · 𝑧))) |
120 | 109 | oveq2d 7229 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝑢( ·𝑠
‘𝑁)𝑤)) |
121 | 119, 120 | eqtr3d 2779 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘(𝑢 · 𝑧)) = (𝑢( ·𝑠
‘𝑁)𝑤)) |
122 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → (𝑣( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑣 · 𝑧))) |
123 | 98, 102, 106, 122 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑣( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘(𝑣 · 𝑧))) |
124 | 109 | oveq2d 7229 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑣( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝑣( ·𝑠
‘𝑁)𝑤)) |
125 | 123, 124 | eqtr3d 2779 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘(𝑣 · 𝑧)) = (𝑣( ·𝑠
‘𝑁)𝑤)) |
126 | 121, 125 | oveq12d 7231 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘(𝑢 · 𝑧))(+g‘𝑁)(𝐹‘(𝑣 · 𝑧))) = ((𝑢( ·𝑠
‘𝑁)𝑤)(+g‘𝑁)(𝑣( ·𝑠
‘𝑁)𝑤))) |
127 | 113, 118,
126 | 3eqtr2d 2783 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘((𝑢(+g‘(Scalar‘𝑀))𝑣) · 𝑧)) = ((𝑢( ·𝑠
‘𝑁)𝑤)(+g‘𝑁)(𝑣( ·𝑠
‘𝑁)𝑤))) |
128 | 108, 110,
127 | 3eqtr3d 2785 |
. . 3
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤) = ((𝑢( ·𝑠
‘𝑁)𝑤)(+g‘𝑁)(𝑣( ·𝑠
‘𝑁)𝑤))) |
129 | 95 | 3ad2antr3 1192 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) → ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤) |
130 | 128, 129 | r19.29a 3208 |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+g‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤) = ((𝑢( ·𝑠
‘𝑁)𝑤)(+g‘𝑁)(𝑣( ·𝑠
‘𝑁)𝑤))) |
131 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘(Scalar‘𝑀)) =
(.r‘(Scalar‘𝑀)) |
132 | 8, 11, 131 | lmodmcl 19911 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → (𝑢(.r‘(Scalar‘𝑀))𝑣) ∈ 𝑆) |
133 | 99, 101, 102, 132 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢(.r‘(Scalar‘𝑀))𝑣) ∈ 𝑆) |
134 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢(.r‘(Scalar‘𝑀))𝑣) ∈ 𝑆 ∧ 𝑧 ∈ 𝑉) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧))) |
135 | 98, 133, 106, 134 | syl3anc 1373 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = (𝐹‘((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧))) |
136 | 109 | oveq2d 7229 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)(𝐹‘𝑧)) = ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤)) |
137 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆 ∧ (𝑣 · 𝑧) ∈ 𝑉) → (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑣 · 𝑧))) = (𝐹‘(𝑢 · (𝑣 · 𝑧)))) |
138 | 98, 101, 116, 137 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑣 · 𝑧))) = (𝐹‘(𝑢 · (𝑣 · 𝑧)))) |
139 | 123 | oveq2d 7229 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)(𝐹‘𝑧))) = (𝑢( ·𝑠
‘𝑁)(𝐹‘(𝑣 · 𝑧)))) |
140 | 2, 8, 26, 11, 131 | lmodvsass 19924 |
. . . . . . . 8
⊢ ((𝑀 ∈ LMod ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉)) → ((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧) = (𝑢 · (𝑣 · 𝑧))) |
141 | 99, 101, 102, 106, 140 | syl13anc 1374 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧) = (𝑢 · (𝑣 · 𝑧))) |
142 | 141 | fveq2d 6721 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧)) = (𝐹‘(𝑢 · (𝑣 · 𝑧)))) |
143 | 138, 139,
142 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘((𝑢(.r‘(Scalar‘𝑀))𝑣) · 𝑧)) = (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)(𝐹‘𝑧)))) |
144 | 135, 136,
143 | 3eqtr3d 2785 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤) = (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)(𝐹‘𝑧)))) |
145 | 124 | oveq2d 7229 |
. . . 4
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)(𝐹‘𝑧))) = (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)𝑤))) |
146 | 144, 145 | eqtrd 2777 |
. . 3
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) ∧ 𝑧 ∈ 𝑉) ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤) = (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)𝑤))) |
147 | 146, 129 | r19.29a 3208 |
. 2
⊢ ((𝜑 ∧ (𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(.r‘(Scalar‘𝑀))𝑣)( ·𝑠
‘𝑁)𝑤) = (𝑢( ·𝑠
‘𝑁)(𝑣(
·𝑠 ‘𝑁)𝑤))) |
148 | | simplll 775 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → 𝜑) |
149 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘(Scalar‘𝑀)) =
(1r‘(Scalar‘𝑀)) |
150 | 11, 149 | ringidcl 19586 |
. . . . . . 7
⊢
((Scalar‘𝑀)
∈ Ring → (1r‘(Scalar‘𝑀)) ∈ 𝑆) |
151 | 17, 150 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(1r‘(Scalar‘𝑀)) ∈ 𝑆) |
152 | 151 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) →
(1r‘(Scalar‘𝑀)) ∈ 𝑆) |
153 | | simplr 769 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → 𝑥 ∈ 𝑉) |
154 | 1, 3, 4, 5, 8, 11,
26, 27, 28 | imasvscaval 17043 |
. . . . 5
⊢ ((𝜑 ∧
(1r‘(Scalar‘𝑀)) ∈ 𝑆 ∧ 𝑥 ∈ 𝑉) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)(𝐹‘𝑥)) = (𝐹‘((1r‘(Scalar‘𝑀)) · 𝑥))) |
155 | 148, 152,
153, 154 | syl3anc 1373 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)(𝐹‘𝑥)) = (𝐹‘((1r‘(Scalar‘𝑀)) · 𝑥))) |
156 | | simpr 488 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → (𝐹‘𝑥) = 𝑢) |
157 | 156 | oveq2d 7229 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)(𝐹‘𝑥)) =
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)𝑢)) |
158 | 5 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → 𝑀 ∈ LMod) |
159 | 2, 8, 26, 149 | lmodvs1 19927 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ 𝑉) →
((1r‘(Scalar‘𝑀)) · 𝑥) = 𝑥) |
160 | 158, 153,
159 | syl2anc 587 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) →
((1r‘(Scalar‘𝑀)) · 𝑥) = 𝑥) |
161 | 160 | fveq2d 6721 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → (𝐹‘((1r‘(Scalar‘𝑀)) · 𝑥)) = (𝐹‘𝑥)) |
162 | 161, 156 | eqtrd 2777 |
. . . 4
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) → (𝐹‘((1r‘(Scalar‘𝑀)) · 𝑥)) = 𝑢) |
163 | 155, 157,
162 | 3eqtr3d 2785 |
. . 3
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ∈ 𝑉) ∧ (𝐹‘𝑥) = 𝑢) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)𝑢) = 𝑢) |
164 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵) |
165 | 82 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ran 𝐹 = 𝐵) |
166 | 164, 165 | eleqtrrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ ran 𝐹) |
167 | | fvelrnb 6773 |
. . . . 5
⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
168 | 167 | biimpa 480 |
. . . 4
⊢ ((𝐹 Fn 𝑉 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢) |
169 | 79, 166, 168 | syl2an2r 685 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢) |
170 | 163, 169 | r19.29a 3208 |
. 2
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) →
((1r‘(Scalar‘𝑀))( ·𝑠
‘𝑁)𝑢) = 𝑢) |
171 | 6, 7, 9, 10, 12, 13, 14, 15, 17, 25, 35, 97, 130, 147, 170 | islmodd 19905 |
1
⊢ (𝜑 → 𝑁 ∈ LMod) |