Metamath Proof Explorer

Theorem lincvalpr

Description: The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019)

Ref Expression
Hypotheses lincvalsn.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincvalsn.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lincvalsn.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
lincvalsn.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
lincvalpr.p ⊢ + = ( +g ‘ 𝑀 )
lincvalpr.f ⊢ 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ }
Assertion lincvalpr ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( ( 𝑋 · 𝑉 ) + ( 𝑌 · 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 lincvalsn.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincvalsn.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 lincvalsn.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
4 lincvalsn.t ⊢ · = ( ·𝑠 ‘ 𝑀 )
5 lincvalpr.p ⊢ + = ( +g ‘ 𝑀 )
6 lincvalpr.f ⊢ 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ }
7 simpl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → 𝑀 ∈ LMod )
8 7 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑀 ∈ LMod )
9 2 fveq2i ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
10 3 9 eqtri ⊢ 𝑅 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
11 10 eleq2i ⊢ ( 𝑋 ∈ 𝑅 ↔ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 11 biimpi ⊢ ( 𝑋 ∈ 𝑅 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
13 12 anim2i ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
14 13 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 10 eleq2i ⊢ ( 𝑌 ∈ 𝑅 ↔ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
16 15 biimpi ⊢ ( 𝑌 ∈ 𝑅 → 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
17 16 anim2i ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
18 17 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
19 fvexd ⊢ ( 𝑀 ∈ LMod → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
20 19 anim2i ⊢ ( ( 𝑉 ≠ 𝑊 ∧ 𝑀 ∈ LMod ) → ( 𝑉 ≠ 𝑊 ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) )
21 20 ancoms ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → ( 𝑉 ≠ 𝑊 ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) )
22 21 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ≠ 𝑊 ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) )
23 6 mapprop ⊢ ( ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ∧ ( 𝑉 ≠ 𝑊 ∧ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 , 𝑊 } ) )
24 14 18 22 23 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 , 𝑊 } ) )
25 1 eleq2i ⊢ ( 𝑉 ∈ 𝐵 ↔ 𝑉 ∈ ( Base ‘ 𝑀 ) )
26 25 biimpi ⊢ ( 𝑉 ∈ 𝐵 → 𝑉 ∈ ( Base ‘ 𝑀 ) )
27 26 adantr ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑉 ∈ ( Base ‘ 𝑀 ) )
28 1 eleq2i ⊢ ( 𝑊 ∈ 𝐵 ↔ 𝑊 ∈ ( Base ‘ 𝑀 ) )
29 28 biimpi ⊢ ( 𝑊 ∈ 𝐵 → 𝑊 ∈ ( Base ‘ 𝑀 ) )
30 29 adantr ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑊 ∈ ( Base ‘ 𝑀 ) )
31 prelpwi ⊢ ( ( 𝑉 ∈ ( Base ‘ 𝑀 ) ∧ 𝑊 ∈ ( Base ‘ 𝑀 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
32 27 30 31 syl2an ⊢ ( ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
33 32 3adant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
34 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 , 𝑊 } ) ∧ { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
35 8 24 33 34 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
36 lmodcmn ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
37 36 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → 𝑀 ∈ CMnd )
38 37 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑀 ∈ CMnd )
39 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → 𝑉 ≠ 𝑊 )
40 simpl ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑉 ∈ 𝐵 )
41 simpl ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑊 ∈ 𝐵 )
42 39 40 41 3anim123i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) )
43 3anrot ⊢ ( ( 𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ↔ ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) )
44 42 43 sylib ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) )
45 6 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } )
46 45 fveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) )
47 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑉 ∈ 𝐵 )
48 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑋 ∈ 𝑅 )
49 39 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
50 fvpr1g ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊 ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
51 47 48 49 50 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
52 46 51 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = 𝑋 )
53 52 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
54 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑀 ∈ LMod )
55 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
56 1 2 55 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
57 54 48 47 56 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
58 53 57 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
59 58 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
60 6 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } )
61 60 fveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) )
62 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 ∈ 𝐵 )
63 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ 𝑅 )
64 39 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
65 fvpr2g ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊 ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
66 62 63 64 65 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
67 61 66 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = 𝑌 )
68 67 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) )
69 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑀 ∈ LMod )
70 1 2 55 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
71 69 63 62 70 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
72 68 71 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
73 72 3adant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
74 fveq2 ⊢ ( 𝑣 = 𝑉 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑉 ) )
75 id ⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
76 74 75 oveq12d ⊢ ( 𝑣 = 𝑉 → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
77 fveq2 ⊢ ( 𝑣 = 𝑊 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑊 ) )
78 id ⊢ ( 𝑣 = 𝑊 → 𝑣 = 𝑊 )
79 77 78 oveq12d ⊢ ( 𝑣 = 𝑊 → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) )
80 1 5 76 79 gsumpr ⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) ∧ ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 ) ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) )
81 38 44 59 73 80 syl112anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) )
82 4 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → · = ( ·𝑠 ‘ 𝑀 ) )
83 82 eqcomd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ·𝑠 ‘ 𝑀 ) = · )
84 6 fveq1i ⊢ ( 𝐹 ‘ 𝑉 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 )
85 40 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ∈ 𝐵 )
86 simpr ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑋 ∈ 𝑅 )
87 86 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑋 ∈ 𝑅 )
88 39 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
89 85 87 88 50 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
90 84 89 syl5eq ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = 𝑋 )
91 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 = 𝑉 )
92 83 90 91 oveq123d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑋 · 𝑉 ) )
93 6 fveq1i ⊢ ( 𝐹 ‘ 𝑊 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 )
94 41 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 ∈ 𝐵 )
95 simpr ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑌 ∈ 𝑅 )
96 95 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ 𝑅 )
97 94 96 88 65 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
98 93 97 syl5eq ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = 𝑌 )
99 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 = 𝑊 )
100 83 98 99 oveq123d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) = ( 𝑌 · 𝑊 ) )
101 92 100 oveq12d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) = ( ( 𝑋 · 𝑉 ) + ( 𝑌 · 𝑊 ) ) )
102 35 81 101 3eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( ( 𝑋 · 𝑉 ) + ( 𝑌 · 𝑊 ) ) )