Theorem islindf2

Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	islindf.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	islindf.v	⊢ · = ( ·𝑠 ‘ 𝑊 )
	islindf.k	⊢ 𝐾 = ( LSpan ‘ 𝑊 )
	islindf.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	islindf.n	⊢ 𝑁 = ( Base ‘ 𝑆 )
	islindf.z	⊢ 0 = ( 0g ‘ 𝑆 )
Assertion	islindf2	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islindf.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		islindf.v	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		islindf.k	⊢ 𝐾 = ( LSpan ‘ 𝑊 )
4		islindf.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5		islindf.n	⊢ 𝑁 = ( Base ‘ 𝑆 )
6		islindf.z	⊢ 0 = ( 0g ‘ 𝑆 )
7		simp1	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝑊 ∈ 𝑌 )
8		simp3	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
9		simp2	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ 𝑋 )
10	8 9	fexd	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 ∈ V )
11	1 2 3 4 5 6	islindf	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
12	7 10 11	syl2anc	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
13		ffdm	⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐼 ) )
14	13	simpld	⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → 𝐹 : dom 𝐹 ⟶ 𝐵 )
15	14	3ad2ant3	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )
16	15	biantrurd	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
17		fdm	⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → dom 𝐹 = 𝐼 )
18	17	3ad2ant3	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → dom 𝐹 = 𝐼 )
19	18	difeq1d	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( dom 𝐹 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑥 } ) )
20	19	imaeq2d	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) )
21	20	fveq2d	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
22	21	eleq2d	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
23	22	notbid	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
24	23	ralbidv	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
25	18 24	raleqbidv	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
26	12 16 25	3bitr2d	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )