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 )