MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islindf Structured version   Visualization version   GIF version

Theorem islindf 21218
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.
StepHypRef Expression
1 feq1 6649 . . . . . 6 (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
21adantr 481 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3 dmeq 5859 . . . . . . 7 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
43adantr 481 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5 fveq2 6842 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6 islindf.b . . . . . . . 8 𝐵 = (Base‘𝑊)
75, 6eqtr4di 2794 . . . . . . 7 (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
87adantl 482 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
94, 8feq23d 6663 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
102, 9bitrd 278 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
11 fvex 6855 . . . . . 6 (Scalar‘𝑤) ∈ V
12 fveq2 6842 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13 fveq2 6842 . . . . . . . . . 10 (𝑠 = (Scalar‘𝑤) → (0g𝑠) = (0g‘(Scalar‘𝑤)))
1413sneqd 4598 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → {(0g𝑠)} = {(0g‘(Scalar‘𝑤))})
1512, 14difeq12d 4083 . . . . . . . 8 (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
1615raleqdv 3313 . . . . . . 7 (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1716ralbidv 3174 . . . . . 6 (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1811, 17sbcie 3782 . . . . 5 ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19 fveq2 6842 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20 islindf.s . . . . . . . . . . . 12 𝑆 = (Scalar‘𝑊)
2119, 20eqtr4di 2794 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
2221fveq2d 6846 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23 islindf.n . . . . . . . . . 10 𝑁 = (Base‘𝑆)
2422, 23eqtr4di 2794 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
2521fveq2d 6846 . . . . . . . . . . 11 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g𝑆))
26 islindf.z . . . . . . . . . . 11 0 = (0g𝑆)
2725, 26eqtr4di 2794 . . . . . . . . . 10 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
2827sneqd 4598 . . . . . . . . 9 (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
2924, 28difeq12d 4083 . . . . . . . 8 (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
3029adantl 482 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31 fveq2 6842 . . . . . . . . . . . 12 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
32 islindf.v . . . . . . . . . . . 12 · = ( ·𝑠𝑊)
3331, 32eqtr4di 2794 . . . . . . . . . . 11 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
3433adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → ( ·𝑠𝑤) = · )
35 eqidd 2737 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → 𝑘 = 𝑘)
36 fveq1 6841 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
3736adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓𝑥) = (𝐹𝑥))
3834, 35, 37oveq123d 7378 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑘( ·𝑠𝑤)(𝑓𝑥)) = (𝑘 · (𝐹𝑥)))
39 fveq2 6842 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40 islindf.k . . . . . . . . . . . 12 𝐾 = (LSpan‘𝑊)
4139, 40eqtr4di 2794 . . . . . . . . . . 11 (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
4241adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43 imaeq1 6008 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
443difeq1d 4081 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
4544imaeq2d 6013 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4643, 45eqtrd 2776 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4746adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4842, 47fveq12d 6849 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
4938, 48eleq12d 2832 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5049notbid 317 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → (¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5130, 50raleqbidv 3319 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
524, 51raleqbidv 3319 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5318, 52bitrid 282 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5410, 53anbi12d 631 . . 3 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55 df-lindf 21212 . . 3 LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
5654, 55brabga 5491 . 2 ((𝐹𝑋𝑊𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
5756ancoms 459 1 ((𝑊𝑌𝐹𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  [wsbc 3739  cdif 3907  {csn 4586   class class class wbr 5105  dom cdm 5633  cima 5636  wf 6492  cfv 6496  (class class class)co 7357  Basecbs 17083  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321  LSpanclspn 20432   LIndF clindf 21210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-lindf 21212
This theorem is referenced by:  islinds2  21219  islindf2  21220  lindff  21221  lindfind  21222  f1lindf  21228  lsslindf  21236  lindfpropd  32169  matunitlindf  36076
  Copyright terms: Public domain W3C validator