Theorem islindf 21794

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 6640	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
2	1	adantr 481	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3		dmeq 5852	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	adantr 481	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5		fveq2 6834	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6		islindf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
7	5, 6	eqtr4di 2793	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
8	7	adantl 482	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
9	4, 8	feq23d 6657	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
10	2, 9	bitrd 280	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
11		fvex 6847	. . . . . 6 ⊢ (Scalar‘𝑤) ∈ V
12		fveq2 6834	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑠 = (Scalar‘𝑤) → (0g‘𝑠) = (0g‘(Scalar‘𝑤)))
14	13	sneqd 4574	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → {(0g‘𝑠)} = {(0g‘(Scalar‘𝑤))})
15	12, 14	difeq12d 4065	. . . . . . . 8 ⊢ (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g‘𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
16	15	raleqdv 3298	. . . . . . 7 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
17	16	ralbidv 3163	. . . . . 6 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
18	11, 17	sbcie 3771	. . . . 5 ⊢ ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20		islindf.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑊)
21	19, 20	eqtr4di 2793	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
22	21	fveq2d 6838	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23		islindf.n	. . . . . . . . . 10 ⊢ 𝑁 = (Base‘𝑆)
24	22, 23	eqtr4di 2793	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
25	21	fveq2d 6838	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g‘𝑆))
26		islindf.z	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑆)
27	25, 26	eqtr4di 2793	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
28	27	sneqd 4574	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
29	24, 28	difeq12d 4065	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
30	29	adantl 482	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
32		islindf.v	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
33	31, 32	eqtr4di 2793	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
34	33	adantl 482	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑤) = · )
35		eqidd 2741	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → 𝑘 = 𝑘)
36		fveq1 6833	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
37	36	adantr 481	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓‘𝑥) = (𝐹‘𝑥))
38	34, 35, 37	oveq123d 7384	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) = (𝑘 · (𝐹‘𝑥)))
39		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40		islindf.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (LSpan‘𝑊)
41	39, 40	eqtr4di 2793	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
42	41	adantl 482	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43		imaeq1 6014	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
44	3	difeq1d 4063	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
45	44	imaeq2d 6019	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
46	43, 45	eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
47	46	adantr 481	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
48	42, 47	fveq12d 6841	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
49	38, 48	eleq12d 2834	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
50	49	notbid 319	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
51	30, 50	raleqbidv 3314	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
52	4, 51	raleqbidv 3314	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
53	18, 52	bitrid 284	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
54	10, 53	anbi12d 638	. . 3 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55		df-lindf 21788	. . 3 ⊢ LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
56	54, 55	brabga 5483	. 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
57	56	ancoms 459	1 ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3054  [wsbc 3730   ∖ cdif 3887  {csn 4562   class class class wbr 5079  dom cdm 5625   “ cima 5628  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  Scalarcsca 17221   ·_𝑠 cvsca 17222  0_gc0g 17400  LSpanclspn 20968   LIndF clindf 21786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-lindf 21788

This theorem is referenced by:  islinds2  21795  islindf2  21796  lindff  21797  lindfind  21798  f1lindf  21804  lsslindf  21812  lindfpropd  33472  matunitlindf  37992