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

Theorem islindf 20132
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 6013 . . . . . 6 (𝑓 = 𝐹 → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
21adantr 481 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝑓⟶(Base‘𝑤)))
3 dmeq 5313 . . . . . . 7 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
43adantr 481 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → dom 𝑓 = dom 𝐹)
5 fveq2 6178 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
6 islindf.b . . . . . . . 8 𝐵 = (Base‘𝑊)
75, 6syl6eqr 2672 . . . . . . 7 (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵)
87adantl 482 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (Base‘𝑤) = 𝐵)
94, 8feq23d 6027 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝐹:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
102, 9bitrd 268 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓:dom 𝑓⟶(Base‘𝑤) ↔ 𝐹:dom 𝐹𝐵))
11 fvex 6188 . . . . . 6 (Scalar‘𝑤) ∈ V
12 fveq2 6178 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → (Base‘𝑠) = (Base‘(Scalar‘𝑤)))
13 fveq2 6178 . . . . . . . . . 10 (𝑠 = (Scalar‘𝑤) → (0g𝑠) = (0g‘(Scalar‘𝑤)))
1413sneqd 4180 . . . . . . . . 9 (𝑠 = (Scalar‘𝑤) → {(0g𝑠)} = {(0g‘(Scalar‘𝑤))})
1512, 14difeq12d 3721 . . . . . . . 8 (𝑠 = (Scalar‘𝑤) → ((Base‘𝑠) ∖ {(0g𝑠)}) = ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}))
1615raleqdv 3139 . . . . . . 7 (𝑠 = (Scalar‘𝑤) → (∀𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1716ralbidv 2983 . . . . . 6 (𝑠 = (Scalar‘𝑤) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))))
1811, 17sbcie 3464 . . . . 5 ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))
19 fveq2 6178 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
20 islindf.s . . . . . . . . . . . 12 𝑆 = (Scalar‘𝑊)
2119, 20syl6eqr 2672 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑆)
2221fveq2d 6182 . . . . . . . . . 10 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑆))
23 islindf.n . . . . . . . . . 10 𝑁 = (Base‘𝑆)
2422, 23syl6eqr 2672 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝑁)
2521fveq2d 6182 . . . . . . . . . . 11 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = (0g𝑆))
26 islindf.z . . . . . . . . . . 11 0 = (0g𝑆)
2725, 26syl6eqr 2672 . . . . . . . . . 10 (𝑤 = 𝑊 → (0g‘(Scalar‘𝑤)) = 0 )
2827sneqd 4180 . . . . . . . . 9 (𝑤 = 𝑊 → {(0g‘(Scalar‘𝑤))} = { 0 })
2924, 28difeq12d 3721 . . . . . . . 8 (𝑤 = 𝑊 → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
3029adantl 482 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) = (𝑁 ∖ { 0 }))
31 fveq2 6178 . . . . . . . . . . . 12 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
32 islindf.v . . . . . . . . . . . 12 · = ( ·𝑠𝑊)
3331, 32syl6eqr 2672 . . . . . . . . . . 11 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
3433adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → ( ·𝑠𝑤) = · )
35 eqidd 2621 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → 𝑘 = 𝑘)
36 fveq1 6177 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
3736adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓𝑥) = (𝐹𝑥))
3834, 35, 37oveq123d 6656 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑘( ·𝑠𝑤)(𝑓𝑥)) = (𝑘 · (𝐹𝑥)))
39 fveq2 6178 . . . . . . . . . . . 12 (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
40 islindf.k . . . . . . . . . . . 12 𝐾 = (LSpan‘𝑊)
4139, 40syl6eqr 2672 . . . . . . . . . . 11 (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝐾)
4241adantl 482 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (LSpan‘𝑤) = 𝐾)
43 imaeq1 5449 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝑓 ∖ {𝑥})))
443difeq1d 3719 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (dom 𝑓 ∖ {𝑥}) = (dom 𝐹 ∖ {𝑥}))
4544imaeq2d 5454 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝐹 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4643, 45eqtrd 2654 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4746adantr 481 . . . . . . . . . 10 ((𝑓 = 𝐹𝑤 = 𝑊) → (𝑓 “ (dom 𝑓 ∖ {𝑥})) = (𝐹 “ (dom 𝐹 ∖ {𝑥})))
4842, 47fveq12d 6184 . . . . . . . . 9 ((𝑓 = 𝐹𝑤 = 𝑊) → ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) = (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))
4938, 48eleq12d 2693 . . . . . . . 8 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5049notbid 308 . . . . . . 7 ((𝑓 = 𝐹𝑤 = 𝑊) → (¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5130, 50raleqbidv 3147 . . . . . 6 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
524, 51raleqbidv 3147 . . . . 5 ((𝑓 = 𝐹𝑤 = 𝑊) → (∀𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘(Scalar‘𝑤)) ∖ {(0g‘(Scalar‘𝑤))}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5318, 52syl5bb 272 . . . 4 ((𝑓 = 𝐹𝑤 = 𝑊) → ([(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))) ↔ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥})))))
5410, 53anbi12d 746 . . 3 ((𝑓 = 𝐹𝑤 = 𝑊) → ((𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥})))) ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
55 df-lindf 20126 . . 3 LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
5654, 55brabga 4979 . 2 ((𝐹𝑋𝑊𝑌) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
5756ancoms 469 1 ((𝑊𝑌𝐹𝑋) → (𝐹 LIndF 𝑊 ↔ (𝐹:dom 𝐹𝐵 ∧ ∀𝑥 ∈ dom 𝐹𝑘 ∈ (𝑁 ∖ { 0 }) ¬ (𝑘 · (𝐹𝑥)) ∈ (𝐾‘(𝐹 “ (dom 𝐹 ∖ {𝑥}))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wral 2909  [wsbc 3429  cdif 3564  {csn 4168   class class class wbr 4644  dom cdm 5104  cima 5107  wf 5872  cfv 5876  (class class class)co 6635  Basecbs 15838  Scalarcsca 15925   ·𝑠 cvsca 15926  0gc0g 16081  LSpanclspn 18952   LIndF clindf 20124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-ov 6638  df-lindf 20126
This theorem is referenced by:  islinds2  20133  islindf2  20134  lindff  20135  lindfind  20136  f1lindf  20142  lsslindf  20150  matunitlindf  33378
  Copyright terms: Public domain W3C validator