Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  f1lindf Structured version   Unicode version

Theorem f1lindf 27283
 Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Assertion
Ref Expression
f1lindf LIndF LIndF

Proof of Theorem f1lindf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2438 . . . . . . 7
21lindff 27276 . . . . . 6 LIndF
32ancoms 441 . . . . 5 LIndF
433adant3 978 . . . 4 LIndF
5 f1f 5642 . . . . 5
653ad2ant3 981 . . . 4 LIndF
7 fco 5603 . . . 4
84, 6, 7syl2anc 644 . . 3 LIndF
9 ffdm 5608 . . . 4
109simpld 447 . . 3
118, 10syl 16 . 2 LIndF
12 simpl2 962 . . . . 5 LIndF Scalar Scalar LIndF
136adantr 453 . . . . . . 7 LIndF
14 fdm 5598 . . . . . . . . . 10
158, 14syl 16 . . . . . . . . 9 LIndF
1615eleq2d 2505 . . . . . . . 8 LIndF
1716biimpa 472 . . . . . . 7 LIndF
1813, 17ffvelrnd 5874 . . . . . 6 LIndF
1918adantrr 699 . . . . 5 LIndF Scalar Scalar
20 eldifi 3471 . . . . . 6 Scalar Scalar Scalar
2120ad2antll 711 . . . . 5 LIndF Scalar Scalar Scalar
22 eldifsni 3930 . . . . . 6 Scalar Scalar Scalar
2322ad2antll 711 . . . . 5 LIndF Scalar Scalar Scalar
24 eqid 2438 . . . . . 6
25 eqid 2438 . . . . . 6
26 eqid 2438 . . . . . 6 Scalar Scalar
27 eqid 2438 . . . . . 6 Scalar Scalar
28 eqid 2438 . . . . . 6 Scalar Scalar
2924, 25, 26, 27, 28lindfind 27277 . . . . 5 LIndF Scalar Scalar
3012, 19, 21, 23, 29syl22anc 1186 . . . 4 LIndF Scalar Scalar
31 f1fn 5643 . . . . . . . . . . 11
32313ad2ant3 981 . . . . . . . . . 10 LIndF
3332adantr 453 . . . . . . . . 9 LIndF
34 fvco2 5801 . . . . . . . . 9
3533, 17, 34syl2anc 644 . . . . . . . 8 LIndF
3635oveq2d 6100 . . . . . . 7 LIndF
3736eleq1d 2504 . . . . . 6 LIndF
38 simpl1 961 . . . . . . . . 9 LIndF
39 imassrn 5219 . . . . . . . . . . 11
40 frn 5600 . . . . . . . . . . . 12
414, 40syl 16 . . . . . . . . . . 11 LIndF
4239, 41syl5ss 3361 . . . . . . . . . 10 LIndF
4342adantr 453 . . . . . . . . 9 LIndF
44 imaco 5378 . . . . . . . . . 10
4515difeq1d 3466 . . . . . . . . . . . . . . 15 LIndF
4645imaeq2d 5206 . . . . . . . . . . . . . 14 LIndF
47 df-f1 5462 . . . . . . . . . . . . . . . . 17
4847simprbi 452 . . . . . . . . . . . . . . . 16
49483ad2ant3 981 . . . . . . . . . . . . . . 15 LIndF
50 imadif 5531 . . . . . . . . . . . . . . 15
5149, 50syl 16 . . . . . . . . . . . . . 14 LIndF
5246, 51eqtrd 2470 . . . . . . . . . . . . 13 LIndF
5352adantr 453 . . . . . . . . . . . 12 LIndF
54 fnsnfv 5789 . . . . . . . . . . . . . . 15
5532, 54sylan 459 . . . . . . . . . . . . . 14 LIndF
5655difeq2d 3467 . . . . . . . . . . . . 13 LIndF
57 imassrn 5219 . . . . . . . . . . . . . . 15
586adantr 453 . . . . . . . . . . . . . . . 16 LIndF
59 frn 5600 . . . . . . . . . . . . . . . 16
6058, 59syl 16 . . . . . . . . . . . . . . 15 LIndF
6157, 60syl5ss 3361 . . . . . . . . . . . . . 14 LIndF
6261ssdifd 3485 . . . . . . . . . . . . 13 LIndF
6356, 62eqsstr3d 3385 . . . . . . . . . . . 12 LIndF
6453, 63eqsstrd 3384 . . . . . . . . . . 11 LIndF
65 imass2 5243 . . . . . . . . . . 11
6664, 65syl 16 . . . . . . . . . 10 LIndF
6744, 66syl5eqss 3394 . . . . . . . . 9 LIndF
681, 25lspss 16065 . . . . . . . . 9
6938, 43, 67, 68syl3anc 1185 . . . . . . . 8 LIndF
7017, 69syldan 458 . . . . . . 7 LIndF
7170sseld 3349 . . . . . 6 LIndF
7237, 71sylbid 208 . . . . 5 LIndF
7372adantrr 699 . . . 4 LIndF Scalar Scalar
7430, 73mtod 171 . . 3 LIndF Scalar Scalar
7574ralrimivva 2800 . 2 LIndF Scalar Scalar
76 simp1 958 . . 3 LIndF
77 rellindf 27269 . . . . . 6 LIndF
7877brrelexi 4921 . . . . 5 LIndF
79783ad2ant2 980 . . . 4 LIndF
80 simp3 960 . . . . . 6 LIndF
81 dmexg 5133 . . . . . . 7
8279, 81syl 16 . . . . . 6 LIndF
83 f1dmex 5974 . . . . . 6
8480, 82, 83syl2anc 644 . . . . 5 LIndF
85 fex 5972 . . . . 5
866, 84, 85syl2anc 644 . . . 4 LIndF
87 coexg 5415 . . . 4
8879, 86, 87syl2anc 644 . . 3 LIndF
891, 24, 25, 26, 28, 27islindf 27273 . . 3 LIndF Scalar Scalar
9076, 88, 89syl2anc 644 . 2 LIndF LIndF Scalar Scalar
9111, 75, 90mpbir2and 890 1 LIndF LIndF
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726   wne 2601  wral 2707  cvv 2958   cdif 3319   wss 3322  csn 3816   class class class wbr 4215  ccnv 4880   cdm 4881   crn 4882  cima 4884   ccom 4885   wfun 5451   wfn 5452  wf 5453  wf1 5454  cfv 5457  (class class class)co 6084  cbs 13474  Scalarcsca 13537  cvsca 13538  c0g 13728  clmod 15955  clspn 16052   LIndF clindf 27265 This theorem is referenced by:  lindfres  27284  f1linds  27286 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-riota 6552  df-slot 13478  df-base 13479  df-0g 13732  df-mnd 14695  df-grp 14817  df-lmod 15957  df-lss 16014  df-lsp 16053  df-lindf 27267
 Copyright terms: Public domain W3C validator