Theorem lincscmcl

Description: The multiplication of a linear combination with a scalar is a linear combination, see also the proof in Lang p. 129. (Contributed by AV, 11-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lincscmcl.s	⊢ · = ( ·𝑠 ‘ 𝑀 )
	lincscmcl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
Assertion	lincscmcl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lincscmcl.s	⊢ · = ( ·𝑠 ‘ 𝑀 )
2		lincscmcl.r	⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
3		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
5	3 4 2	lcoval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
6	5	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ( 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
7		simpl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑀 ∈ LMod )
8	7	ad2antrr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → 𝑀 ∈ LMod )
9		simpr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → 𝐶 ∈ 𝑅 )
10	9	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → 𝐶 ∈ 𝑅 )
11		simprl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → 𝐷 ∈ ( Base ‘ 𝑀 ) )
12	3 4 1 2	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐶 · 𝐷 ) ∈ ( Base ‘ 𝑀 ) )
13	8 10 11 12	syl3anc	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 · 𝐷 ) ∈ ( Base ‘ 𝑀 ) )
14	4	lmodring	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
15	14	ad2antrr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
16	15	adantl	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
17	16	adantr	⊢ ( ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( Scalar ‘ 𝑀 ) ∈ Ring )
18	9	adantl	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → 𝐶 ∈ 𝑅 )
19	18	adantr	⊢ ( ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝐶 ∈ 𝑅 )
20		elmapi	⊢ ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑥 : 𝑉 ⟶ 𝑅 )
21		ffvelcdm	⊢ ( ( 𝑥 : 𝑉 ⟶ 𝑅 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 )
22	21	ex	⊢ ( 𝑥 : 𝑉 ⟶ 𝑅 → ( 𝑣 ∈ 𝑉 → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 ) )
23	20 22	syl	⊢ ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑣 ∈ 𝑉 → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 ) )
24	23	adantr	⊢ ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 ) )
25	24	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 ) )
26	25	imp	⊢ ( ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 )
27		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ ( Scalar ‘ 𝑀 ) )
28	2 27	ringcl	⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 𝐶 ∈ 𝑅 ∧ ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 ) → ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ∈ 𝑅 )
29	17 19 26 28	syl3anc	⊢ ( ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ∈ 𝑅 )
30	29	fmpttd	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) : 𝑉 ⟶ 𝑅 )
31	2	fvexi	⊢ 𝑅 ∈ V
32		simpr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
33	32	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
34	33	adantl	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
35		elmapg	⊢ ( ( 𝑅 ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ∈ ( 𝑅 ↑m 𝑉 ) ↔ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) : 𝑉 ⟶ 𝑅 ) )
36	31 34 35	sylancr	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ∈ ( 𝑅 ↑m 𝑉 ) ↔ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) : 𝑉 ⟶ 𝑅 ) )
37	30 36	mpbird	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ∈ ( 𝑅 ↑m 𝑉 ) )
38	15 33 9	3jca	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐶 ∈ 𝑅 ) )
39	38	adantl	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐶 ∈ 𝑅 ) )
40		simpl	⊢ ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) )
41	40	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) )
42		simprl	⊢ ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
43	42	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
44	2	rmfsupp	⊢ ( ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐶 ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
45	39 41 43 44	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
46		oveq2	⊢ ( 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝐶 · 𝐷 ) = ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
47	46	adantl	⊢ ( ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐶 · 𝐷 ) = ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
48	47	adantl	⊢ ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 · 𝐷 ) = ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
49	48	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝐶 · 𝐷 ) = ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) )
50		simprl	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
51	40	adantr	⊢ ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) )
52	51 9	anim12i	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐶 ∈ 𝑅 ) )
53		eqid	⊢ ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 )
54		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) )
55	1 27 53 2 54	lincscm	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐶 ∈ 𝑅 ) ∧ 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
56	50 52 43 55	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝐶 · ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
57	49 56	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ( 𝐶 · 𝐷 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
58		breq1	⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) → ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
59		oveq1	⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) → ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
60	59	eqeq2d	⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) → ( ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( 𝐶 · 𝐷 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) )
61	58 60	anbi12d	⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
62	61	rspcev	⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ ( Scalar ‘ 𝑀 ) ) ( 𝑥 ‘ 𝑣 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
63	37 45 57 62	syl12anc	⊢ ( ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
64	63	ex	⊢ ( ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ∧ 𝐷 ∈ ( Base ‘ 𝑀 ) ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
65	64	ex	⊢ ( ( 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
66	65	rexlimiva	⊢ ( ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( 𝐷 ∈ ( Base ‘ 𝑀 ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
67	66	impcom	⊢ ( ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
68	67	impcom	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
69	3 4 2	lcoval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 𝐶 · 𝐷 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
70	69	ad2antrr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 𝐶 · 𝐷 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝐶 · 𝐷 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
71	13 68 70	mpbir2and	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) ∧ ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )
72	71	ex	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ( ( 𝐷 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ ( 𝑅 ↑m 𝑉 ) ( 𝑥 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝐷 = ( 𝑥 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
73	6 72	sylbid	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ) → ( 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) ) )
74	73	3impia	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ ( 𝑀 LinCo 𝑉 ) ) → ( 𝐶 · 𝐷 ) ∈ ( 𝑀 LinCo 𝑉 ) )