Metamath Proof Explorer

Theorem linc1

Description: A vector is a linear combination of a set containing this vector. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses linc1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
linc1.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
linc1.0 ⊢ 0 = ( 0g ‘ 𝑆 )
linc1.1 ⊢ 1 = ( 1r ‘ 𝑆 )
linc1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
Assertion linc1 ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 linc1.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 linc1.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 linc1.0 ⊢ 0 = ( 0g ‘ 𝑆 )
4 linc1.1 ⊢ 1 = ( 1r ‘ 𝑆 )
5 linc1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) )
6 simp1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑀 ∈ LMod )
7 2 lmodring ⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Ring )
8 2 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = 𝑆
9 8 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
10 9 4 ringidcl ⊢ ( 𝑆 ∈ Ring → 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
11 9 3 ring0cl ⊢ ( 𝑆 ∈ Ring → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 10 11 jca ⊢ ( 𝑆 ∈ Ring → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
13 7 12 syl ⊢ ( 𝑀 ∈ LMod → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
14 13 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 14 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
16 ifcl ⊢ ( ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → if ( 𝑥 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
17 15 16 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → if ( 𝑥 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
18 17 5 fmptd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
19 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
20 simp2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑉 ∈ 𝒫 𝐵 )
21 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
22 19 20 21 sylancr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
23 18 22 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
24 1 pweqi ⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
25 24 eleq2i ⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
26 25 biimpi ⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
27 26 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
28 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
29 6 23 27 28 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) )
30 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
31 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
32 grpmnd ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
33 31 32 syl ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
34 33 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑀 ∈ Mnd )
35 simp3 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
36 6 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → 𝑀 ∈ LMod )
37 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑋 ↔ 𝑦 = 𝑋 ) )
38 37 ifbid ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 𝑋 , 1 , 0 ) = if ( 𝑦 = 𝑋 , 1 , 0 ) )
39 simpr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
40 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
41 2 40 4 lmod1cl ⊢ ( 𝑀 ∈ LMod → 1 ∈ ( Base ‘ 𝑆 ) )
42 41 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 1 ∈ ( Base ‘ 𝑆 ) )
43 42 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → 1 ∈ ( Base ‘ 𝑆 ) )
44 2 40 3 lmod0cl ⊢ ( 𝑀 ∈ LMod → 0 ∈ ( Base ‘ 𝑆 ) )
45 44 3ad2ant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 0 ∈ ( Base ‘ 𝑆 ) )
46 45 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → 0 ∈ ( Base ‘ 𝑆 ) )
47 43 46 ifcld ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ ( Base ‘ 𝑆 ) )
48 5 38 39 47 fvmptd3 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 𝑋 , 1 , 0 ) )
49 48 47 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
50 elelpwi ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑦 ∈ 𝐵 )
51 50 expcom ⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑦 ∈ 𝑉 → 𝑦 ∈ 𝐵 ) )
52 51 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑉 → 𝑦 ∈ 𝐵 ) )
53 52 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝐵 )
54 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
55 1 2 54 40 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
56 36 49 53 55 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
57 eqid ⊢ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
58 56 57 fmptd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) : 𝑉 ⟶ 𝐵 )
59 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑣 ) )
60 id ⊢ ( 𝑦 = 𝑣 → 𝑦 = 𝑣 )
61 59 60 oveq12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
62 61 cbvmptv ⊢ ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
63 fvexd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 0g ‘ 𝑀 ) ∈ V )
64 ovexd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ V )
65 62 20 63 64 mptsuppd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑣 ∈ 𝑉 ∣ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) } )
66 2a1 ⊢ ( 𝑣 = 𝑋 → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) ) )
67 simprr ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → 𝑣 ∈ 𝑉 )
68 4 fvexi ⊢ 1 ∈ V
69 3 fvexi ⊢ 0 ∈ V
70 68 69 ifex ⊢ if ( 𝑣 = 𝑋 , 1 , 0 ) ∈ V
71 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑋 ↔ 𝑣 = 𝑋 ) )
72 71 ifbid ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑋 , 1 , 0 ) = if ( 𝑣 = 𝑋 , 1 , 0 ) )
73 72 5 fvmptg ⊢ ( ( 𝑣 ∈ 𝑉 ∧ if ( 𝑣 = 𝑋 , 1 , 0 ) ∈ V ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑋 , 1 , 0 ) )
74 67 70 73 sylancl ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑋 , 1 , 0 ) )
75 iffalse ⊢ ( ¬ 𝑣 = 𝑋 → if ( 𝑣 = 𝑋 , 1 , 0 ) = 0 )
76 75 adantr ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → if ( 𝑣 = 𝑋 , 1 , 0 ) = 0 )
77 74 76 eqtrd ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝐹 ‘ 𝑣 ) = 0 )
78 77 oveq1d ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
79 6 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
80 79 adantl ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → 𝑀 ∈ LMod )
81 elelpwi ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑣 ∈ 𝐵 )
82 81 expcom ⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
83 82 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
84 83 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
85 84 adantl ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → 𝑣 ∈ 𝐵 )
86 1 2 54 3 30 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0g ‘ 𝑀 ) )
87 80 85 86 syl2anc ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0g ‘ 𝑀 ) )
88 78 87 eqtrd ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0g ‘ 𝑀 ) )
89 88 neeq1d ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) ) )
90 eqneqall ⊢ ( ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) → ( ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) )
91 30 90 ax-mp ⊢ ( ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 )
92 89 91 syl6bi ⊢ ( ( ¬ 𝑣 = 𝑋 ∧ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) )
93 92 ex ⊢ ( ¬ 𝑣 = 𝑋 → ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) ) )
94 66 93 pm2.61i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) )
95 94 ralrimiva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ∀ 𝑣 ∈ 𝑉 ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) )
96 rabsssn ⊢ ( { 𝑣 ∈ 𝑉 ∣ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑋 } ↔ ∀ 𝑣 ∈ 𝑉 ( ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) → 𝑣 = 𝑋 ) )
97 95 96 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → { 𝑣 ∈ 𝑉 ∣ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑋 } )
98 65 97 eqsstrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ { 𝑋 } )
99 1 30 34 20 35 58 98 gsumpt ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 Σg ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ‘ 𝑋 ) )
100 ovex ⊢ ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ V
101 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑋 ) )
102 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
103 101 102 oveq12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
104 103 57 fvmptg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) ∈ V ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
105 35 100 104 sylancl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
106 iftrue ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝑋 , 1 , 0 ) = 1 )
107 106 5 fvmptg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 1 ∈ V ) → ( 𝐹 ‘ 𝑋 ) = 1 )
108 35 68 107 sylancl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) = 1 )
109 108 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) )
110 elelpwi ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑋 ∈ 𝐵 )
111 110 ancoms ⊢ ( ( 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
112 111 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
113 1 2 54 4 lmodvs1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑋 )
114 6 112 113 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑋 ) = 𝑋 )
115 105 109 114 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑦 ) ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ‘ 𝑋 ) = 𝑋 )
116 29 99 115 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑋 )