Theorem islindf 21844

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

Hypotheses

Ref	Expression
islindf.b	⊢ 𝐵 = (Base‘𝑊)
islindf.v	⊢ · = ( ·𝑠 ‘𝑊)
islindf.k	⊢ 𝐾 = (LSpan‘𝑊)
islindf.s	⊢ 𝑆 = (Scalar‘𝑊)
islindf.n	⊢ 𝑁 = (Base‘𝑆)
islindf.z	⊢ 0 = (0g‘𝑆)

Assertion

Ref	Expression
islindf	⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))

Distinct variable groups:   𝑘,𝐹,𝑥   𝑘,𝑁   𝑘,𝑊,𝑥   0 ,𝑘

Allowed substitution hints:   𝐵(𝑥,𝑘)   𝑆(𝑥,𝑘)   · (𝑥,𝑘)   𝐾(𝑥,𝑘)   𝑁(𝑥)   𝑋(𝑥,𝑘)   𝑌(𝑥,𝑘)   0 (𝑥)

Proof of Theorem islindf

Dummy variables 𝑓 𝑤 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		feq1 6665	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
2	1	adantr 484	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3		dmeq 5877	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	adantr 484	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5		fveq2 6863	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6		islindf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
7	5, 6	eqtr4di 2814	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
8	7	adantl 485	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
9	4, 8	feq23d 6682	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
10	2, 9	bitrd 281	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
11		fvex 6876	. . . . . 6 ⊢ (Scalar‘𝑤) ∈ V
12		fveq2 6863	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13		fveq2 6863	. . . . . . . . . 10 ⊢ (𝑠 = (Scalar‘𝑤) → (0g‘𝑠) = (0g‘(Scalar‘𝑤)))
14	13	sneqd 4593	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → {(0g‘𝑠)} = {(0g‘(Scalar‘𝑤))})
15	12, 14	difeq12d 4081	. . . . . . . 8 ⊢ (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g‘𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
16	15	raleqdv 3319	. . . . . . 7 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
17	16	ralbidv 3184	. . . . . 6 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
18	11, 17	sbcie 3785	. . . . 5 ⊢ ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19		fveq2 6863	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20		islindf.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑊)
21	19, 20	eqtr4di 2814	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
22	21	fveq2d 6867	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23		islindf.n	. . . . . . . . . 10 ⊢ 𝑁 = (Base‘𝑆)
24	22, 23	eqtr4di 2814	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
25	21	fveq2d 6867	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g‘𝑆))
26		islindf.z	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑆)
27	25, 26	eqtr4di 2814	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
28	27	sneqd 4593	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
29	24, 28	difeq12d 4081	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
30	29	adantl 485	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31		fveq2 6863	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
32		islindf.v	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
33	31, 32	eqtr4di 2814	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
34	33	adantl 485	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑤) = · )
35		eqidd 2762	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → 𝑘 = 𝑘)
36		fveq1 6862	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
37	36	adantr 484	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓‘𝑥) = (𝐹‘𝑥))
38	34, 35, 37	oveq123d 7413	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) = (𝑘 · (𝐹‘𝑥)))
39		fveq2 6863	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40		islindf.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (LSpan‘𝑊)
41	39, 40	eqtr4di 2814	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
42	41	adantl 485	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43		imaeq1 6041	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
44	3	difeq1d 4079	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
45	44	imaeq2d 6046	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
46	43, 45	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
47	46	adantr 484	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
48	42, 47	fveq12d 6870	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
49	38, 48	eleq12d 2855	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
50	49	notbid 320	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
51	30, 50	raleqbidv 3335	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
52	4, 51	raleqbidv 3335	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
53	18, 52	bitrid 285	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
54	10, 53	anbi12d 641	. . 3 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55		df-lindf 21838	. . 3 ⊢ LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
56	54, 55	brabga 5503	. 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
57	56	ancoms 462	1 ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  [wsbc 3744   ∖ cdif 3901  {csn 4581   class class class wbr 5099  dom cdm 5645   “ cima 5648  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  Basecbs 17228  Scalarcsca 17272   ·_𝑠 cvsca 17273  0_gc0g 17451  LSpanclspn 21018   LIndF clindf 21836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-ov 7395  df-lindf 21838

This theorem is referenced by:  islinds2  21845  islindf2  21846  lindff  21847  lindfind  21848  f1lindf  21854  lsslindf  21862  lindfpropd  33529  matunitlindf  38081