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	$⊢ φ \to N = F “_{𝑠} M$
	imaslmod.v	$⊢ V = {Base}_{M}$
	imaslmod.k	$⊢ S = {Base}_{Scalar (M)}$
	imaslmod.p	$⊢ \underset{˙}{+} = +_{M}$
	imaslmod.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	imaslmod.o	$⊢ \underset{˙}{0} = 0_{M}$
	imaslmod.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imaslmod.e1	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{+} b) = F (p \underset{˙}{+} q))$
	imaslmod.e2	$⊢ (φ \land (k \in S \land a \in V \land b \in V)) \to (F (a) = F (b) \to F (k \underset{˙}{\cdot} a) = F (k \underset{˙}{\cdot} b))$
	imaslmod.l	$⊢ φ \to M \in LMod$
Assertion	imaslmod	$⊢ φ \to N \in LMod$

Proof

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

Metamath Proof Explorer

Theorem imaslmod

Proof