Theorem islindf

Description: Property of an independent family of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

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

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		feq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ) )
8	7	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ) )
9		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
10	9	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → dom 𝑓 = dom 𝐹 )
11		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
12	11 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
13	12	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( Base ‘ 𝑤 ) = 𝐵 )
14	10 13	feq23d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝐹 ⟶ 𝐵 ) )
15	8 14	bitrd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝐹 ⟶ 𝐵 ) )
16		fvex	⊢ ( Scalar ‘ 𝑤 ) ∈ V
17		fveq2	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( Base ‘ 𝑠 ) = ( Base ‘ ( Scalar ‘ 𝑤 ) ) )
18		fveq2	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( 0g ‘ 𝑠 ) = ( 0g ‘ ( Scalar ‘ 𝑤 ) ) )
19	18	sneqd	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → { ( 0g ‘ 𝑠 ) } = { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } )
20	17 19	difeq12d	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) = ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) )
21	20	raleqdv	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) )
22	21	ralbidv	⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) )
23	16 22	sbcie	⊢ ( [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) )
24		fveq2	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
25	24 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝑆 )
26	25	fveq2d	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝑆 ) )
27	26 5	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝑁 )
28	25	fveq2d	⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = ( 0g ‘ 𝑆 ) )
29	28 6	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = 0 )
30	29	sneqd	⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } = { 0 } )
31	27 30	difeq12d	⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) = ( 𝑁 ∖ { 0 } ) )
32	31	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) = ( 𝑁 ∖ { 0 } ) )
33		fveq2	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
34	33 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
35	34	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ·𝑠 ‘ 𝑤 ) = · )
36		eqidd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → 𝑘 = 𝑘 )
37		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
38	37	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
39	35 36 38	oveq123d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) = ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) )
40		fveq2	⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
41	40 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝐾 )
42	41	adantl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( LSpan ‘ 𝑤 ) = 𝐾 )
43		imaeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝑓 ∖ { 𝑥 } ) ) )
44	9	difeq1d	⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 ∖ { 𝑥 } ) = ( dom 𝐹 ∖ { 𝑥 } ) )
45	44	imaeq2d	⊢ ( 𝑓 = 𝐹 → ( 𝐹 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
46	43 45	eqtrd	⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
47	46	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
48	42 47	fveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
49	39 48	eleq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
50	49	notbid	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
51	32 50	raleqbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
52	10 51	raleqbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
53	23 52	bitrid	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
54	15 53	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ∧ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
55		df-lindf	⊢ LIndF = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ∧ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) }
56	54 55	brabga	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
57	56	ancoms	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )