Metamath Proof Explorer

Theorem lindfrn

Description: The range of an independent family is an independent set. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion lindfrn ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 1 lindff ⊢ ( ( 𝐹 LIndF 𝑊 ∧ 𝑊 ∈ LMod ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
3 2 ancoms ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → 𝐹 : dom 𝐹 ⟶ ( Base ‘ 𝑊 ) )
4 3 frnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ⊆ ( Base ‘ 𝑊 ) )
5 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑊 ∈ LMod )
6 imassrn ⊢ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ran 𝐹
7 6 4 sstrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝑊 ) )
8 7 adantr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝑊 ) )
9 3 ffund ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → Fun 𝐹 )
10 eldifsn ⊢ ( 𝑥 ∈ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) ) )
11 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
12 fvelrnb ⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ dom 𝐹 ( 𝐹 ‘ 𝑘 ) = 𝑥 ) )
13 11 12 sylbi ⊢ ( Fun 𝐹 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ dom 𝐹 ( 𝐹 ‘ 𝑘 ) = 𝑥 ) )
14 13 adantr ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑘 ∈ dom 𝐹 ( 𝐹 ‘ 𝑘 ) = 𝑥 ) )
15 difss ⊢ ( dom 𝐹 ∖ { 𝑦 } ) ⊆ dom 𝐹
16 15 jctr ⊢ ( Fun 𝐹 → ( Fun 𝐹 ∧ ( dom 𝐹 ∖ { 𝑦 } ) ⊆ dom 𝐹 ) )
17 16 ad2antrr ⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → ( Fun 𝐹 ∧ ( dom 𝐹 ∖ { 𝑦 } ) ⊆ dom 𝐹 ) )
18 simpl ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → 𝑘 ∈ dom 𝐹 )
19 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑦 ) )
20 19 necon3i ⊢ ( ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) → 𝑘 ≠ 𝑦 )
21 20 adantl ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → 𝑘 ≠ 𝑦 )
22 eldifsn ⊢ ( 𝑘 ∈ ( dom 𝐹 ∖ { 𝑦 } ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝑘 ≠ 𝑦 ) )
23 18 21 22 sylanbrc ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → 𝑘 ∈ ( dom 𝐹 ∖ { 𝑦 } ) )
24 23 adantl ⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → 𝑘 ∈ ( dom 𝐹 ∖ { 𝑦 } ) )
25 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( dom 𝐹 ∖ { 𝑦 } ) ⊆ dom 𝐹 ) → ( 𝑘 ∈ ( dom 𝐹 ∖ { 𝑦 } ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
26 17 24 25 sylc ⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) )
27 26 expr ⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
28 neeq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = 𝑥 → ( ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) ) )
29 eleq1 ⊢ ( ( 𝐹 ‘ 𝑘 ) = 𝑥 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ↔ 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
30 28 29 imbi12d ⊢ ( ( 𝐹 ‘ 𝑘 ) = 𝑥 → ( ( ( 𝐹 ‘ 𝑘 ) ≠ ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ↔ ( 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ) )
31 27 30 syl5ibcom ⊢ ( ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ∧ 𝑘 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑘 ) = 𝑥 → ( 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ) )
32 31 rexlimdva ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ∃ 𝑘 ∈ dom 𝐹 ( 𝐹 ‘ 𝑘 ) = 𝑥 → ( 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ) )
33 14 32 sylbid ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑥 ∈ ran 𝐹 → ( 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) ) )
34 33 impd ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑥 ≠ ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
35 10 34 syl5bi ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝑥 ∈ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) → 𝑥 ∈ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
36 35 ssrdv ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) )
37 9 36 sylan ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) )
38 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
39 1 38 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝑊 ) ∧ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ⊆ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
40 5 8 37 39 syl3anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
41 40 adantrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
42 simplr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝐹 LIndF 𝑊 )
43 simprl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑦 ∈ dom 𝐹 )
44 eldifi ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45 44 ad2antll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
46 eldifsni ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
47 46 ad2antll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
48 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
49 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
50 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
51 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
52 48 38 49 50 51 lindfind ⊢ ( ( ( 𝐹 LIndF 𝑊 ∧ 𝑦 ∈ dom 𝐹 ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
53 42 43 45 47 52 syl22anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑦 } ) ) ) )
54 41 53 ssneldd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) ∧ ( 𝑦 ∈ dom 𝐹 ∧ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) )
55 54 ralrimivva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ∀ 𝑦 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) )
56 9 funfnd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → 𝐹 Fn dom 𝐹 )
57 oveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) )
58 sneq ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → { 𝑥 } = { ( 𝐹 ‘ 𝑦 ) } )
59 58 difeq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ran 𝐹 ∖ { 𝑥 } ) = ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) )
60 59 fveq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) )
61 57 60 eleq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ↔ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ) )
62 61 notbid ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ) )
63 62 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ) )
64 63 ralrn ⊢ ( 𝐹 Fn dom 𝐹 → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ) )
65 56 64 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ dom 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { ( 𝐹 ‘ 𝑦 ) } ) ) ) )
66 55 65 mpbird ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) )
67 1 48 38 49 51 50 islinds2 ⊢ ( 𝑊 ∈ LMod → ( ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( ran 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ) ) )
68 67 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( ran 𝐹 ⊆ ( Base ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ran 𝐹 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( ran 𝐹 ∖ { 𝑥 } ) ) ) ) )
69 4 66 68 mpbir2and ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) )