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

Theorem islindf2 20428
Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-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
islindf2 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥𝐼𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
Distinct variable groups:   𝑘,𝐹,𝑥   𝑘,𝑁   𝑘,𝑊,𝑥   0 ,𝑘   𝐵,𝑘,𝑥   𝑘,𝐼,𝑥   𝑘,𝑋,𝑥   𝑘,𝑌,𝑥
Allowed substitution hints:   𝑆(𝑥,𝑘)   · (𝑥,𝑘)   𝐾(𝑥,𝑘)   𝑁(𝑥)   0 (𝑥)

Proof of Theorem islindf2
StepHypRef Expression
1 simp1 1166 . . 3 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → 𝑊𝑌)
2 simp3 1168 . . . 4 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → 𝐹:𝐼𝐵)
3 simp2 1167 . . . 4 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → 𝐼𝑋)
4 fex 6681 . . . 4 ((𝐹:𝐼𝐵𝐼𝑋) → 𝐹 ∈ V)
52, 3, 4syl2anc 579 . . 3 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → 𝐹 ∈ V)
6 islindf.b . . . 4 𝐵 = (Base‘𝑊)
7 islindf.v . . . 4 · = ( ·𝑠𝑊)
8 islindf.k . . . 4 𝐾 = (LSpan‘𝑊)
9 islindf.s . . . 4 𝑆 = (Scalar‘𝑊)
10 islindf.n . . . 4 𝑁 = (Base‘𝑆)
11 islindf.z . . . 4 0 = (0g𝑆)
126, 7, 8, 9, 10, 11islindf 20426 . . 3 ((𝑊𝑌𝐹 ∈ V) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
131, 5, 12syl2anc 579 . 2 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
14 ffdm 6243 . . . . 5 (𝐹:𝐼𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐼))
1514simpld 488 . . . 4 (𝐹:𝐼𝐵𝐹:dom 𝐹𝐵)
16153ad2ant3 1165 . . 3 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → 𝐹:dom 𝐹𝐵)
1716biantrurd 528 . 2 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
18 fdm 6230 . . . 4 (𝐹:𝐼𝐵 → dom 𝐹 = 𝐼)
19183ad2ant3 1165 . . 3 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → dom 𝐹 = 𝐼)
2019difeq1d 3888 . . . . . . . 8 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (dom 𝐹 ∖ {𝑥}) = (𝐼 ∖ {𝑥}))
2120imaeq2d 5647 . . . . . . 7 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (𝐹 “ (dom 𝐹 ∖ {𝑥})) = (𝐹 “ (𝐼 ∖ {𝑥})))
2221fveq2d 6378 . . . . . 6 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥}))))
2322eleq2d 2829 . . . . 5 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → ((𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
2423notbid 309 . . . 4 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
2524ralbidv 3132 . . 3 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
2619, 25raleqbidv 3299 . 2 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))) ↔ ∀𝑥𝐼𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
2713, 17, 263bitr2d 298 1 ((𝑊𝑌𝐼𝑋𝐹:𝐼𝐵) → (𝐹 LIndF 𝑊 ↔ ∀𝑥𝐼𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (𝐼 ∖ {𝑥})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3054  Vcvv 3349  cdif 3728  wss 3731  {csn 4333   class class class wbr 4808  dom cdm 5276  cima 5279  wf 6063  cfv 6067  (class class class)co 6841  Basecbs 16131  Scalarcsca 16218   ·𝑠 cvsca 16219  0gc0g 16367  LSpanclspn 19242   LIndF clindf 20418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-lindf 20420
This theorem is referenced by:  lindfmm  20441  islindf4  20452
  Copyright terms: Public domain W3C validator