Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  linindslinci Structured version   Unicode version

Theorem linindslinci 32531
 Description: The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.)
Hypotheses
Ref Expression
islininds.b
islininds.z
islininds.r Scalar
islininds.e
islininds.0
Assertion
Ref Expression
linindslinci linIndS finSupp linC
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()

Proof of Theorem linindslinci
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 islininds.b . . . 4
2 islininds.z . . . 4
3 islininds.r . . . 4 Scalar
4 islininds.e . . . 4
5 islininds.0 . . . 4
61, 2, 3, 4, 5linindsi 32530 . . 3 linIndS finSupp linC
7 breq1 4456 . . . . . . . . . 10 finSupp finSupp
8 oveq1 6302 . . . . . . . . . . 11 linC linC
98eqeq1d 2469 . . . . . . . . . 10 linC linC
107, 9anbi12d 710 . . . . . . . . 9 finSupp linC finSupp linC
11 fveq1 5871 . . . . . . . . . . 11
1211eqeq1d 2469 . . . . . . . . . 10
1312ralbidv 2906 . . . . . . . . 9
1410, 13imbi12d 320 . . . . . . . 8 finSupp linC finSupp linC
1514rspcv 3215 . . . . . . 7 finSupp linC finSupp linC
1615com23 78 . . . . . 6 finSupp linC finSupp linC
17163impib 1194 . . . . 5 finSupp linC finSupp linC
1817com12 31 . . . 4 finSupp linC finSupp linC
1918adantl 466 . . 3 finSupp linC finSupp linC
206, 19syl 16 . 2 linIndS finSupp linC
2120imp 429 1 linIndS finSupp linC
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 973   wceq 1379   wcel 1767  wral 2817  cpw 4016   class class class wbr 4453  cfv 5594  (class class class)co 6295   cmap 7432   finSupp cfsupp 7841  cbs 14507  Scalarcsca 14575  c0g 14712   linC clinc 32487   linIndS clininds 32523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-xp 5011  df-rel 5012  df-iota 5557  df-fv 5602  df-ov 6298  df-lininds 32525 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator