Metamath Proof Explorer

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 ffvelrn ⊢ ( ( 𝑥 : 𝑉 ⟶ 𝑅 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ‘ 𝑣 ) ∈ 𝑅 )
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 𝑉 ) )