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 birani ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑉 ∈ ( Base ‘ 𝑀 ) )
27 1 eleq2i ⊢ ( 𝑊 ∈ 𝐵 ↔ 𝑊 ∈ ( Base ‘ 𝑀 ) )
28 27 birani ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑊 ∈ ( Base ‘ 𝑀 ) )
29 prelpwi ⊢ ( ( 𝑉 ∈ ( Base ‘ 𝑀 ) ∧ 𝑊 ∈ ( Base ‘ 𝑀 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
30 26 28 29 syl2an ⊢ ( ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
31 30 3adant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) )
32 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m { 𝑉 , 𝑊 } ) ∧ { 𝑉 , 𝑊 } ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
33 8 24 31 32 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
34 lmodcmn ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ CMnd )
35 34 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → 𝑀 ∈ CMnd )
36 35 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑀 ∈ CMnd )
37 simpr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) → 𝑉 ≠ 𝑊 )
38 simpl ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑉 ∈ 𝐵 )
39 simpl ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑊 ∈ 𝐵 )
40 37 38 39 3anim123i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) )
41 3anrot ⊢ ( ( 𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ↔ ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) )
42 40 41 sylib ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) )
43 6 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } )
44 43 fveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) )
45 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑉 ∈ 𝐵 )
46 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑋 ∈ 𝑅 )
47 37 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
48 fvpr1g ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊 ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
49 45 46 47 48 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
50 44 49 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = 𝑋 )
51 50 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
52 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → 𝑀 ∈ LMod )
53 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
54 1 2 53 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
55 52 46 45 54 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
56 51 55 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
57 56 3adant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 )
58 6 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝐹 = { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } )
59 58 fveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) )
60 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 ∈ 𝐵 )
61 simprr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ 𝑅 )
62 37 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
63 fvpr2g ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊 ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
64 60 61 62 63 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
65 59 64 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = 𝑌 )
66 65 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) = ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) )
67 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑀 ∈ LMod )
68 1 2 53 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
69 67 61 60 68 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
70 66 69 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
71 70 3adant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 )
72 fveq2 ⊢ ( 𝑣 = 𝑉 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑉 ) )
73 id ⊢ ( 𝑣 = 𝑉 → 𝑣 = 𝑉 )
74 72 73 oveq12d ⊢ ( 𝑣 = 𝑉 → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
75 fveq2 ⊢ ( 𝑣 = 𝑊 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑊 ) )
76 id ⊢ ( 𝑣 = 𝑊 → 𝑣 = 𝑊 )
77 75 76 oveq12d ⊢ ( 𝑣 = 𝑊 → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) )
78 1 5 74 77 gsumpr ⊢ ( ( 𝑀 ∈ CMnd ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊 ) ∧ ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ∈ 𝐵 ) ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) )
79 36 42 57 71 78 syl112anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑀 Σg ( 𝑣 ∈ { 𝑉 , 𝑊 } ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) )
80 4 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → · = ( ·𝑠 ‘ 𝑀 ) )
81 80 eqcomd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ·𝑠 ‘ 𝑀 ) = · )
82 6 fveq1i ⊢ ( 𝐹 ‘ 𝑉 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 )
83 38 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ∈ 𝐵 )
84 simpr ⊢ ( ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) → 𝑋 ∈ 𝑅 )
85 84 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑋 ∈ 𝑅 )
86 37 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 ≠ 𝑊 )
87 83 85 86 48 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑉 ) = 𝑋 )
88 82 87 eqtrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑉 ) = 𝑋 )
89 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑉 = 𝑉 )
90 81 88 89 oveq123d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 𝑋 · 𝑉 ) )
91 6 fveq1i ⊢ ( 𝐹 ‘ 𝑊 ) = ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 )
92 39 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 ∈ 𝐵 )
93 simpr ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) → 𝑌 ∈ 𝑅 )
94 93 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ 𝑅 )
95 92 94 86 63 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( { ⟨ 𝑉 , 𝑋 ⟩ , ⟨ 𝑊 , 𝑌 ⟩ } ‘ 𝑊 ) = 𝑌 )
96 91 95 eqtrid ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ‘ 𝑊 ) = 𝑌 )
97 eqidd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑊 = 𝑊 )
98 81 96 97 oveq123d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) = ( 𝑌 · 𝑊 ) )
99 90 98 oveq12d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( ( 𝐹 ‘ 𝑉 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) + ( ( 𝐹 ‘ 𝑊 ) ( ·𝑠 ‘ 𝑀 ) 𝑊 ) ) = ( ( 𝑋 · 𝑉 ) + ( 𝑌 · 𝑊 ) ) )
100 33 79 99 3eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊 ) ∧ ( 𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 , 𝑊 } ) = ( ( 𝑋 · 𝑉 ) + ( 𝑌 · 𝑊 ) ) )