Metamath Proof Explorer

Theorem imaslmod

Description: The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023)

Ref Expression
Hypotheses imaslmod.u ⊢ ( 𝜑 → 𝑁 = ( 𝐹 “s 𝑀 ) )
imaslmod.v ⊢ 𝑉 = ( Base ‘ 𝑀 )
imaslmod.k ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
imaslmod.p ⊢ + = ( +g ‘ 𝑀 )
imaslmod.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
imaslmod.o ⊢ 0 = ( 0g ‘ 𝑀 )
imaslmod.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imaslmod.e1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imaslmod.e2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑘 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 · 𝑏 ) ) ) )
imaslmod.l ⊢ ( 𝜑 → 𝑀 ∈ LMod )
Assertion imaslmod ( 𝜑 → 𝑁 ∈ LMod )

Proof

Step Hyp Ref Expression
1 imaslmod.u ⊢ ( 𝜑 → 𝑁 = ( 𝐹 “s 𝑀 ) )
2 imaslmod.v ⊢ 𝑉 = ( Base ‘ 𝑀 )
3 imaslmod.k ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
4 imaslmod.p ⊢ + = ( +g ‘ 𝑀 )
5 imaslmod.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
6 imaslmod.o ⊢ 0 = ( 0g ‘ 𝑀 )
7 imaslmod.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
8 imaslmod.e1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
9 imaslmod.e2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑘 · 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 · 𝑏 ) ) ) )
10 imaslmod.l ⊢ ( 𝜑 → 𝑀 ∈ LMod )
11 2 a1i ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑀 ) )
12 1 11 7 10 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑁 ) )
13 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 ) )
14 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
15 1 11 7 10 14 imassca ⊢ ( 𝜑 → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑁 ) )
16 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 ) )
17 3 a1i ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
18 eqidd ⊢ ( 𝜑 → ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ ( Scalar ‘ 𝑀 ) ) )
19 eqidd ⊢ ( 𝜑 → ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ ( Scalar ‘ 𝑀 ) ) )
20 eqidd ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) )
21 14 lmodring ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
22 10 21 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑀 ) ∈ Ring )
23 4 a1i ⊢ ( 𝜑 → + = ( +g ‘ 𝑀 ) )
24 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
25 10 24 syl ⊢ ( 𝜑 → 𝑀 ∈ Grp )
26 1 11 23 7 8 25 6 imasgrp ⊢ ( 𝜑 → ( 𝑁 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑁 ) ) )
27 26 simpld ⊢ ( 𝜑 → 𝑁 ∈ Grp )
28 eqid ⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 )
29 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑀 ∈ LMod )
30 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑘 ∈ 𝑆 )
31 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
32 2 14 5 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑘 · 𝑏 ) ∈ 𝑉 )
33 29 30 31 32 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑘 · 𝑏 ) ∈ 𝑉 )
34 1 11 7 10 14 3 5 28 9 33 imasvscaf ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑁 ) : ( 𝑆 × 𝐵 ) ⟶ 𝐵 )
35 34 fovcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) ∈ 𝐵 )
36 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝜑 )
37 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) )
38 37 simp1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑢 ∈ 𝑆 )
39 38 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝑢 ∈ 𝑆 )
40 36 25 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝑀 ∈ Grp )
41 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝑦 ∈ 𝑉 )
42 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝑧 ∈ 𝑉 )
43 2 4 grpcl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
44 40 41 42 43 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑦 + 𝑧 ) ∈ 𝑉 )
45 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ ( 𝑦 + 𝑧 ) ∈ 𝑉 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑢 · ( 𝑦 + 𝑧 ) ) ) )
46 36 39 44 45 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑢 · ( 𝑦 + 𝑧 ) ) ) )
47 eqid ⊢ ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 )
48 7 8 1 11 10 4 47 imasaddval ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
49 36 41 42 48 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) )
50 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ 𝑦 ) = 𝑣 )
51 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ 𝑧 ) = 𝑤 )
52 50 51 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) )
53 49 52 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) )
54 53 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) ) )
55 36 10 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → 𝑀 ∈ LMod )
56 2 4 14 5 3 lmodvsdi ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑢 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) )
57 55 39 41 42 56 syl13anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) )
58 57 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ ( 𝑢 · ( 𝑦 + 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) ) )
59 46 54 58 3eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) ) )
60 2 14 5 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑢 · 𝑦 ) ∈ 𝑉 )
61 55 39 41 60 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 · 𝑦 ) ∈ 𝑉 )
62 2 14 5 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑢 · 𝑧 ) ∈ 𝑉 )
63 55 39 42 62 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 · 𝑧 ) ∈ 𝑉 )
64 7 8 1 11 10 4 47 imasaddval ⊢ ( ( 𝜑 ∧ ( 𝑢 · 𝑦 ) ∈ 𝑉 ∧ ( 𝑢 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) ) )
65 36 61 63 64 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑦 ) + ( 𝑢 · 𝑧 ) ) ) )
66 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) )
67 36 39 41 66 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) )
68 50 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑦 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) )
69 67 68 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) )
70 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) )
71 36 39 42 70 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) )
72 51 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
73 71 72 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
74 69 73 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑦 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) ( +g ‘ 𝑁 ) ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
75 59 65 74 3eqtr2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝑣 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) ( +g ‘ 𝑁 ) ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
76 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝜑 )
77 37 simp2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑣 ∈ 𝐵 )
78 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
79 7 78 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
80 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
81 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
82 7 81 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) → ran 𝐹 = 𝐵 )
84 80 83 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ ran 𝐹 )
85 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 ) )
86 85 biimpa ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑣 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 )
87 79 84 86 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 )
88 76 77 87 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ∃ 𝑦 ∈ 𝑉 ( 𝐹 ‘ 𝑦 ) = 𝑣 )
89 75 88 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) ( +g ‘ 𝑁 ) ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
90 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
91 82 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ran 𝐹 = 𝐵 )
92 90 91 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ ran 𝐹 )
93 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
94 93 biimpa ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑤 ∈ ran 𝐹 ) → ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 )
95 79 92 94 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 )
96 95 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 )
97 89 96 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( +g ‘ 𝑁 ) 𝑤 ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑣 ) ( +g ‘ 𝑁 ) ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
98 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝜑 )
99 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑀 ∈ LMod )
100 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) )
101 100 simp1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑢 ∈ 𝑆 )
102 100 simp2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑣 ∈ 𝑆 )
103 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ ( Scalar ‘ 𝑀 ) )
104 14 3 103 lmodacl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 )
105 99 101 102 104 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 )
106 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑧 ∈ 𝑉 )
107 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) )
108 98 105 106 107 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) )
109 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = 𝑤 )
110 109 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
111 2 4 14 5 3 103 lmodvsdir ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) = ( ( 𝑢 · 𝑧 ) + ( 𝑣 · 𝑧 ) ) )
112 99 101 102 106 111 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) = ( ( 𝑢 · 𝑧 ) + ( 𝑣 · 𝑧 ) ) )
113 112 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑧 ) + ( 𝑣 · 𝑧 ) ) ) )
114 99 101 106 62 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 · 𝑧 ) ∈ 𝑉 )
115 2 14 5 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑣 · 𝑧 ) ∈ 𝑉 )
116 99 102 106 115 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑣 · 𝑧 ) ∈ 𝑉 )
117 7 8 1 11 10 4 47 imasaddval ⊢ ( ( 𝜑 ∧ ( 𝑢 · 𝑧 ) ∈ 𝑉 ∧ ( 𝑣 · 𝑧 ) ∈ 𝑉 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑧 ) + ( 𝑣 · 𝑧 ) ) ) )
118 98 114 116 117 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) = ( 𝐹 ‘ ( ( 𝑢 · 𝑧 ) + ( 𝑣 · 𝑧 ) ) ) )
119 98 101 106 70 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) )
120 109 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
121 119 120 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
122 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) )
123 98 102 106 122 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) )
124 109 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
125 123 124 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) = ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
126 121 125 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝐹 ‘ ( 𝑢 · 𝑧 ) ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ( +g ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
127 113 118 126 3eqtr2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ( +g ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
128 108 110 127 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ( +g ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
129 95 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝐹 ‘ 𝑧 ) = 𝑤 )
130 128 129 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ( +g ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
131 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ ( Scalar ‘ 𝑀 ) )
132 14 3 131 lmodmcl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 )
133 99 101 102 132 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 )
134 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) )
135 98 133 106 134 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) )
136 109 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) )
137 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ ( 𝑣 · 𝑧 ) ∈ 𝑉 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑢 · ( 𝑣 · 𝑧 ) ) ) )
138 98 101 116 137 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑢 · ( 𝑣 · 𝑧 ) ) ) )
139 123 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ ( 𝑣 · 𝑧 ) ) ) )
140 2 14 5 3 131 lmodvsass ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) = ( 𝑢 · ( 𝑣 · 𝑧 ) ) )
141 99 101 102 106 140 syl13anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) = ( 𝑢 · ( 𝑣 · 𝑧 ) ) )
142 141 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) = ( 𝐹 ‘ ( 𝑢 · ( 𝑣 · 𝑧 ) ) ) )
143 138 139 142 3eqtr4rd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) · 𝑧 ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) ) )
144 135 136 143 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) ) )
145 124 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
146 144 145 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
147 146 129 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑣 ) ( ·𝑠 ‘ 𝑁 ) 𝑤 ) = ( 𝑢 ( ·𝑠 ‘ 𝑁 ) ( 𝑣 ( ·𝑠 ‘ 𝑁 ) 𝑤 ) ) )
148 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → 𝜑 )
149 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) )
150 3 149 ringidcl ⊢ ( ( Scalar ‘ 𝑀 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ 𝑆 )
151 22 150 syl ⊢ ( 𝜑 → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ 𝑆 )
152 151 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ 𝑆 )
153 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → 𝑥 ∈ 𝑉 )
154 1 11 7 10 14 3 5 28 9 imasvscaval ⊢ ( ( 𝜑 ∧ ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ 𝑆 ∧ 𝑥 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) ) )
155 148 152 153 154 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) ) )
156 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( 𝐹 ‘ 𝑥 ) = 𝑢 )
157 156 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) 𝑢 ) )
158 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → 𝑀 ∈ LMod )
159 2 14 5 149 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) = 𝑥 )
160 158 153 159 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) = 𝑥 )
161 160 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( 𝐹 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
162 161 156 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( 𝐹 ‘ ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) · 𝑥 ) ) = 𝑢 )
163 155 157 162 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑢 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) 𝑢 ) = 𝑢 )
164 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
165 82 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ran 𝐹 = 𝐵 )
166 164 165 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ ran 𝐹 )
167 fvelrnb ⊢ ( 𝐹 Fn 𝑉 → ( 𝑢 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 ) )
168 167 biimpa ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑢 ∈ ran 𝐹 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 )
169 79 166 168 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐹 ‘ 𝑥 ) = 𝑢 )
170 163 169 r19.29a ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑁 ) 𝑢 ) = 𝑢 )
171 12 13 15 16 17 18 19 20 22 27 35 97 130 147 170 islmodd ⊢ ( 𝜑 → 𝑁 ∈ LMod )