Metamath Proof Explorer

Theorem isldepslvec2

Description: Alternative definition of being a linearly dependent subset of a (left) vector space. In this case, the reverse implication of islindeps2 holds, so that both definitions are equivalent (see theorem 1.6 in Roman p. 46 and the note in Roman p. 112: if a nontrivial linear combination of elements (where not all of the coefficients are 0) in an R-vector space is 0, then and only then each of the elements is a linear combination of the others. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
islindeps2.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
islindeps2.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
islindeps2.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
islindeps2.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion isldepslvec2 ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ 𝑆 linDepS 𝑀 ) )

Proof

Step Hyp Ref Expression
1 islindeps2.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 islindeps2.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
3 islindeps2.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
4 islindeps2.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
5 islindeps2.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 lveclmod ⊢ ( 𝑀 ∈ LVec → 𝑀 ∈ LMod )
7 6 adantr ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑀 ∈ LMod )
8 simpr ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
9 3 lvecdrng ⊢ ( 𝑀 ∈ LVec → 𝑅 ∈ DivRing )
10 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
11 9 10 syl ⊢ ( 𝑀 ∈ LVec → 𝑅 ∈ NzRing )
12 11 adantr ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → 𝑅 ∈ NzRing )
13 1 2 3 4 5 islindeps2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑅 ∈ NzRing ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑆 linDepS 𝑀 ) )
14 7 8 12 13 syl3anc ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → 𝑆 linDepS 𝑀 ) )
15 1 2 3 4 5 islindeps ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
16 df-3an ⊢ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
17 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
18 16 17 bitr4i ⊢ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
19 18 rexbii ⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
20 rexcom ⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∃ 𝑠 ∈ 𝑆 ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
21 19 20 bitri ⊢ ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
22 simplr ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑆 ∈ 𝒫 𝐵 )
23 6 ad2antrr ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑀 ∈ LMod )
24 simpr ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 )
25 22 23 24 3jca ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆 ) )
26 25 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆 ) )
27 simplr ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) )
28 elmapi ⊢ ( 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) → 𝑔 : 𝑆 ⟶ 𝐸 )
29 ffvelrn ⊢ ( ( 𝑔 : 𝑆 ⟶ 𝐸 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑔 ‘ 𝑠 ) ∈ 𝐸 )
30 28 24 29 syl2anr ⊢ ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( 𝑔 ‘ 𝑠 ) ∈ 𝐸 )
31 simpr ⊢ ( ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → ( 𝑔 ‘ 𝑠 ) ≠ 0 )
32 30 31 anim12i ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( ( 𝑔 ‘ 𝑠 ) ∈ 𝐸 ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) )
33 9 ad2antrr ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑅 ∈ DivRing )
34 33 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → 𝑅 ∈ DivRing )
35 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
36 4 35 5 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( 𝑔 ‘ 𝑠 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝑔 ‘ 𝑠 ) ∈ 𝐸 ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
37 34 36 syl ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( ( 𝑔 ‘ 𝑠 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝑔 ‘ 𝑠 ) ∈ 𝐸 ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) )
38 32 37 mpbird ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑔 ‘ 𝑠 ) ∈ ( Unit ‘ 𝑅 ) )
39 simpll ⊢ ( ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → 𝑔 finSupp 0 )
40 39 adantl ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → 𝑔 finSupp 0 )
41 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
42 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
43 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
44 eqid ⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) )
45 1 3 4 35 5 2 41 42 43 44 lincresunit2 ⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆 ) ∧ ( 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝑔 ‘ 𝑠 ) ∈ ( Unit ‘ 𝑅 ) ∧ 𝑔 finSupp 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 )
46 26 27 38 40 45 syl13anc ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 )
47 simpll ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑀 ∈ LVec )
48 22 47 24 3jca ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆 ) )
49 48 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆 ) )
50 simprr ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑔 ‘ 𝑠 ) ≠ 0 )
51 simplr ⊢ ( ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
52 51 adantl ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 )
53 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑔 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑦 ) )
54 53 oveq2d ⊢ ( 𝑧 = 𝑦 → ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑦 ) ) )
55 54 cbvmptv ⊢ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) = ( 𝑦 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑦 ) ) )
56 1 3 4 35 5 2 41 42 43 55 lincreslvec3 ⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LVec ∧ 𝑠 ∈ 𝑆 ) ∧ ( 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ∧ 𝑔 finSupp 0 ) ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 )
57 49 27 50 40 52 56 syl131anc ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 )
58 1 3 4 35 5 2 41 42 43 44 lincresunit1 ⊢ ( ( ( 𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ LMod ∧ 𝑠 ∈ 𝑆 ) ∧ ( 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ∧ ( 𝑔 ‘ 𝑠 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) )
59 26 27 38 58 syl12anc ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) )
60 breq1 ⊢ ( 𝑓 = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 finSupp 0 ↔ ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ) )
61 oveq1 ⊢ ( 𝑓 = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) )
62 61 eqeq1d ⊢ ( 𝑓 = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ↔ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) )
63 60 62 anbi12d ⊢ ( 𝑓 = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
64 63 adantl ⊢ ( ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) ∧ 𝑓 = ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
65 59 64 rspcedv ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ( ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) finSupp 0 ∧ ( ( 𝑧 ∈ ( 𝑆 ∖ { 𝑠 } ) ↦ ( ( ( invr ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ ( 𝑔 ‘ 𝑠 ) ) ) ( .r ‘ 𝑅 ) ( 𝑔 ‘ 𝑧 ) ) ) ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) → ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
66 46 57 65 mp2and ⊢ ( ( ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) ) → ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) )
67 66 rexlimdva2 ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
68 67 reximdva ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ∧ ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
69 21 68 syl5bi ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ∃ 𝑔 ∈ ( 𝐸 ↑m 𝑆 ) ( 𝑔 finSupp 0 ∧ ( 𝑔 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑔 ‘ 𝑠 ) ≠ 0 ) → ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
70 15 69 sylbid ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( 𝑆 linDepS 𝑀 → ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ) )
71 14 70 impbid ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ 𝒫 𝐵 ) → ( ∃ 𝑠 ∈ 𝑆 ∃ 𝑓 ∈ ( 𝐸 ↑m ( 𝑆 ∖ { 𝑠 } ) ) ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) ( 𝑆 ∖ { 𝑠 } ) ) = 𝑠 ) ↔ 𝑆 linDepS 𝑀 ) )