Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  islbs3 Structured version   Unicode version

Theorem islbs3 16232
 Description: An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
islbs2.v
islbs2.j LBasis
islbs2.n
Assertion
Ref Expression
islbs3
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem islbs3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 islbs2.v . . . . 5
2 islbs2.j . . . . 5 LBasis
31, 2lbsss 16154 . . . 4
5 islbs2.n . . . . 5
61, 2, 5lbssp 16156 . . . 4
8 lveclmod 16183 . . . . . . . 8
983ad2ant1 979 . . . . . . 7
10 pssss 3444 . . . . . . . . 9
1110, 3sylan9ssr 3364 . . . . . . . 8
12113adant1 976 . . . . . . 7
131, 5lspssv 16064 . . . . . . 7
149, 12, 13syl2anc 644 . . . . . 6
15 eqid 2438 . . . . . . . . . 10 Scalar Scalar
1615lvecdrng 16182 . . . . . . . . 9 Scalar
17 eqid 2438 . . . . . . . . . 10 Scalar Scalar
18 eqid 2438 . . . . . . . . . 10 Scalar Scalar
1917, 18drngunz 15855 . . . . . . . . 9 Scalar Scalar Scalar
2016, 19syl 16 . . . . . . . 8 Scalar Scalar
218, 20jca 520 . . . . . . 7 Scalar Scalar
222, 5, 15, 18, 17, 1lbspss 16159 . . . . . . 7 Scalar Scalar
2321, 22syl3an1 1218 . . . . . 6
24 df-pss 3338 . . . . . 6
2514, 23, 24sylanbrc 647 . . . . 5
26253expia 1156 . . . 4
2726alrimiv 1642 . . 3
284, 7, 273jca 1135 . 2
29 simpr1 964 . . 3
30 simpr2 965 . . 3
31 simplr1 1000 . . . . . . . . 9
3231ssdifssd 3487 . . . . . . . 8
33 fvex 5745 . . . . . . . . 9
341, 33eqeltri 2508 . . . . . . . 8
35 ssexg 4352 . . . . . . . 8
3632, 34, 35sylancl 645 . . . . . . 7
37 simplr3 1002 . . . . . . 7
38 difssd 3477 . . . . . . . 8
39 simpr 449 . . . . . . . . . 10
40 neldifsn 3931 . . . . . . . . . 10
41 nelne1 2695 . . . . . . . . . 10
4239, 40, 41sylancl 645 . . . . . . . . 9
4342necomd 2689 . . . . . . . 8
44 df-pss 3338 . . . . . . . 8
4538, 43, 44sylanbrc 647 . . . . . . 7
46 psseq1 3436 . . . . . . . . 9
47 fveq2 5731 . . . . . . . . . 10
4847psseq1d 3441 . . . . . . . . 9
4946, 48imbi12d 313 . . . . . . . 8
5049spcgv 3038 . . . . . . 7
5136, 37, 45, 50syl3c 60 . . . . . 6
52 dfpss3 3435 . . . . . . 7
5352simprbi 452 . . . . . 6
5451, 53syl 16 . . . . 5
55 simplr2 1001 . . . . . . 7
568ad2antrr 708 . . . . . . . 8
5732adantrr 699 . . . . . . . . 9
58 eqid 2438 . . . . . . . . . 10
591, 58, 5lspcl 16057 . . . . . . . . 9
6056, 57, 59syl2anc 644 . . . . . . . 8
61 ssun1 3512 . . . . . . . . . 10
62 undif1 3705 . . . . . . . . . 10
6361, 62sseqtr4i 3383 . . . . . . . . 9
641, 5lspssid 16066 . . . . . . . . . . 11
6556, 57, 64syl2anc 644 . . . . . . . . . 10
66 simprr 735 . . . . . . . . . . 11
6766snssd 3945 . . . . . . . . . 10
6865, 67unssd 3525 . . . . . . . . 9
6963, 68syl5ss 3361 . . . . . . . 8
7058, 5lspssp 16069 . . . . . . . 8
7156, 60, 69, 70syl3anc 1185 . . . . . . 7
7255, 71eqsstr3d 3385 . . . . . 6
7372expr 600 . . . . 5
7454, 73mtod 171 . . . 4
7574ralrimiva 2791 . . 3
761, 2, 5islbs2 16231 . . . 4