Theorem islindf 21721

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 6666	. . . . . 6 ⊢ (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
2	1	adantr 480	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3		dmeq 5867	. . . . . . 7 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	adantr 480	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5		fveq2 6858	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6		islindf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑊)
7	5, 6	eqtr4di 2782	. . . . . . 7 ⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
8	7	adantl 481	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
9	4, 8	feq23d 6683	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
10	2, 9	bitrd 279	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹⟶𝐵))
11		fvex 6871	. . . . . 6 ⊢ (Scalar‘𝑤) ∈ V
12		fveq2 6858	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13		fveq2 6858	. . . . . . . . . 10 ⊢ (𝑠 = (Scalar‘𝑤) → (0g‘𝑠) = (0g‘(Scalar‘𝑤)))
14	13	sneqd 4601	. . . . . . . . 9 ⊢ (𝑠 = (Scalar‘𝑤) → {(0g‘𝑠)} = {(0g‘(Scalar‘𝑤))})
15	12, 14	difeq12d 4090	. . . . . . . 8 ⊢ (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g‘𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
16	15	raleqdv 3299	. . . . . . 7 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
17	16	ralbidv 3156	. . . . . 6 ⊢ (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
18	11, 17	sbcie 3795	. . . . 5 ⊢ ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20		islindf.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑊)
21	19, 20	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
22	21	fveq2d 6862	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23		islindf.n	. . . . . . . . . 10 ⊢ 𝑁 = (Base‘𝑆)
24	22, 23	eqtr4di 2782	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
25	21	fveq2d 6862	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g‘𝑆))
26		islindf.z	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑆)
27	25, 26	eqtr4di 2782	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
28	27	sneqd 4601	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
29	24, 28	difeq12d 4090	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
30	29	adantl 481	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = ( ·𝑠 ‘𝑊))
32		islindf.v	. . . . . . . . . . . 12 ⊢ · = ( ·𝑠 ‘𝑊)
33	31, 32	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → ( ·𝑠 ‘𝑤) = · )
34	33	adantl 481	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ( ·𝑠 ‘𝑤) = · )
35		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → 𝑘 = 𝑘)
36		fveq1 6857	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
37	36	adantr 480	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓‘𝑥) = (𝐹‘𝑥))
38	34, 35, 37	oveq123d 7408	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) = (𝑘 · (𝐹‘𝑥)))
39		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40		islindf.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (LSpan‘𝑊)
41	39, 40	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
42	41	adantl 481	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43		imaeq1 6026	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
44	3	difeq1d 4088	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
45	44	imaeq2d 6031	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
46	43, 45	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
47	46	adantr 480	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
48	42, 47	fveq12d 6865	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
49	38, 48	eleq12d 2822	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
50	49	notbid 318	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
51	30, 50	raleqbidv 3319	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
52	4, 51	raleqbidv 3319	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
53	18, 52	bitrid 283	. . . 4 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
54	10, 53	anbi12d 632	. . 3 ⊢ ((𝑓 = 𝐹 ∧ 𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55		df-lindf 21715	. . 3 ⊢ LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]∀𝑥 ∈ dom 𝑓∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑘( ·𝑠 ‘𝑤)(𝑓‘𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
56	54, 55	brabga 5494	. 2 ⊢ ((𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
57	56	ancoms 458	1 ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹⟶𝐵 ∧ ∀𝑥 ∈ dom 𝐹∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹‘𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  [wsbc 3753   ∖ cdif 3911  {csn 4589   class class class wbr 5107  dom cdm 5638   “ cima 5641  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  Scalarcsca 17223   ·_𝑠 cvsca 17224  0_gc0g 17402  LSpanclspn 20877   LIndF clindf 21713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-lindf 21715

This theorem is referenced by:  islinds2  21722  islindf2  21723  lindff  21724  lindfind  21725  f1lindf  21731  lsslindf  21739  lindfpropd  33353  matunitlindf  37612