Theorem islindf 20673

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 6330	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
2	1	adantr 473	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3		dmeq 5626	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	adantr 473	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5		fveq2 6504	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6		islindf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
7	5, 6	syl6eqr 2834	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
8	7	adantl 474	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
9	4, 8	feq23d 6344	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
10	2, 9	bitrd 271	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
11		fvex 6517	. . . . . 6 ⊢ (Scalar‘𝑤) ∈ V
12		fveq2 6504	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13		fveq2 6504	. . . . . . . . . 10 ⊢ (𝑠 = (Scalar‘𝑤) → (0g‘𝑠) = (0g‘(Scalar‘𝑤)))
14	13	sneqd 4456	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → {(0g‘𝑠)} = {(0g‘(Scalar‘𝑤))})
15	12, 14	difeq12d 3992	. . . . . . . 8 ⊢ (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g‘𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
16	15	raleqdv 3357	. . . . . . 7 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
17	16	ralbidv 3149	. . . . . 6 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
18	11, 17	sbcie 3718	. . . . 5 ⊢ ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19		fveq2 6504	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20		islindf.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑊)
21	19, 20	syl6eqr 2834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
22	21	fveq2d 6508	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23		islindf.n	. . . . . . . . . 10 ⊢ 𝑁 = (Base‘𝑆)
24	22, 23	syl6eqr 2834	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
25	21	fveq2d 6508	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g‘𝑆))
26		islindf.z	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑆)
27	25, 26	syl6eqr 2834	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
28	27	sneqd 4456	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
29	24, 28	difeq12d 3992	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
30	29	adantl 474	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31		fveq2 6504	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
32		islindf.v	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
33	31, 32	syl6eqr 2834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
34	33	adantl 474	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑤) = · )
35		eqidd 2781	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → 𝑘 = 𝑘)
36		fveq1 6503	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
37	36	adantr 473	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓‘𝑥) = (𝐹‘𝑥))
38	34, 35, 37	oveq123d 7003	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) = (𝑘 · (𝐹‘𝑥)))
39		fveq2 6504	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40		islindf.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (LSpan‘𝑊)
41	39, 40	syl6eqr 2834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
42	41	adantl 474	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43		imaeq1 5770	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
44	3	difeq1d 3990	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
45	44	imaeq2d 5775	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
46	43, 45	eqtrd 2816	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
47	46	adantr 473	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
48	42, 47	fveq12d 6511	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
49	38, 48	eleq12d 2862	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
50	49	notbid 310	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
51	30, 50	raleqbidv 3343	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
52	4, 51	raleqbidv 3343	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
53	18, 52	syl5bb 275	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
54	10, 53	anbi12d 622	. . 3 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55		df-lindf 20667	. . 3 ⊢ LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
56	54, 55	brabga 5279	. 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
57	56	ancoms 451	1 ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508   ∈ wcel 2051  ∀wral 3090  [wsbc 3683   ∖ cdif 3828  {csn 4444   class class class wbr 4934  dom cdm 5411   “ cima 5414  ⟶wf 6189  ‘cfv 6193  (class class class)co 6982  Basecbs 16345  Scalarcsca 16430   ·_𝑠 cvsca 16431  0_gc0g 16575  LSpanclspn 19477   LIndF clindf 20665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2752  ax-sep 5064  ax-nul 5071  ax-pr 5190

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2551  df-eu 2589  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3419  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4182  df-if 4354  df-sn 4445  df-pr 4447  df-op 4451  df-uni 4718  df-br 4935  df-opab 4997  df-xp 5417  df-rel 5418  df-cnv 5419  df-co 5420  df-dm 5421  df-rn 5422  df-res 5423  df-ima 5424  df-iota 6157  df-fun 6195  df-fn 6196  df-f 6197  df-fv 6201  df-ov 6985  df-lindf 20667

This theorem is referenced by:  islinds2  20674  islindf2  20675  lindff  20676  lindfind  20677  f1lindf  20683  lsslindf  20691  lindfpropd  30645  matunitlindf  34371