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

Theorem islindf 20886
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 6489 . . . . . 6 (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
21adantr 481 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3 dmeq 5766 . . . . . . 7 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
43adantr 481 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5 fveq2 6664 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6 islindf.b . . . . . . . 8 𝐵 = (Base‘𝑊)
75, 6syl6eqr 2874 . . . . . . 7 (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
87adantl 482 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
94, 8feq23d 6503 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
102, 9bitrd 280 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
11 fvex 6677 . . . . . 6 (Scalar‘𝑤) ∈ V
12 fveq2 6664 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13 fveq2 6664 . . . . . . . . . 10 (𝑠 = (Scalar‘𝑤) → (0g𝑠) = (0g‘(Scalar‘𝑤)))
1413sneqd 4571 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → {(0g𝑠)} = {(0g‘(Scalar‘𝑤))})
1512, 14difeq12d 4099 . . . . . . . 8 (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
1615raleqdv 3416 . . . . . . 7 (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1716ralbidv 3197 . . . . . 6 (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1811, 17sbcie 3811 . . . . 5 ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19 fveq2 6664 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20 islindf.s . . . . . . . . . . . 12 𝑆 = (Scalar‘𝑊)
2119, 20syl6eqr 2874 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
2221fveq2d 6668 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23 islindf.n . . . . . . . . . 10 𝑁 = (Base‘𝑆)
2422, 23syl6eqr 2874 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
2521fveq2d 6668 . . . . . . . . . . 11 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g𝑆))
26 islindf.z . . . . . . . . . . 11 0 = (0g𝑆)
2725, 26syl6eqr 2874 . . . . . . . . . 10 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
2827sneqd 4571 . . . . . . . . 9 (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
2924, 28difeq12d 4099 . . . . . . . 8 (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
3029adantl 482 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31 fveq2 6664 . . . . . . . . . . . 12 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
32 islindf.v . . . . . . . . . . . 12 · = ( ·𝑠𝑊)
3331, 32syl6eqr 2874 . . . . . . . . . . 11 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
3433adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → ( ·𝑠𝑤) = · )
35 eqidd 2822 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → 𝑘 = 𝑘)
36 fveq1 6663 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
3736adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓𝑥) = (𝐹𝑥))
3834, 35, 37oveq123d 7166 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑘( ·𝑠𝑤)(𝑓𝑥)) = (𝑘 · (𝐹𝑥)))
39 fveq2 6664 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40 islindf.k . . . . . . . . . . . 12 𝐾 = (LSpan‘𝑊)
4139, 40syl6eqr 2874 . . . . . . . . . . 11 (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
4241adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43 imaeq1 5918 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
443difeq1d 4097 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
4544imaeq2d 5923 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4643, 45eqtrd 2856 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4746adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4842, 47fveq12d 6671 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
4938, 48eleq12d 2907 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5049notbid 319 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → (¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5130, 50raleqbidv 3402 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
524, 51raleqbidv 3402 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5318, 52syl5bb 284 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5410, 53anbi12d 630 . . 3 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55 df-lindf 20880 . . 3 LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
5654, 55brabga 5413 . 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 207  wa 396   = wceq 1528  wcel 2105  wral 3138  [wsbc 3771  cdif 3932  {csn 4559   class class class wbr 5058  dom cdm 5549  cima 5552  wf 6345  cfv 6349  (class class class)co 7145  Basecbs 16473  Scalarcsca 16558   ·𝑠 cvsca 16559  0gc0g 16703  LSpanclspn 19674   LIndF clindf 20878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-lindf 20880
This theorem is referenced by:  islinds2  20887  islindf2  20888  lindff  20889  lindfind  20890  f1lindf  20896  lsslindf  20904  lindfpropd  30870  matunitlindf  34772
  Copyright terms: Public domain W3C validator