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	biimtrid	⊢ ( ( 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 ‘ 𝑊 ) )