![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > islinds4 | Structured version Visualization version GIF version |
Description: A set is independent in a vector space iff it is a subset of some basis. (AC equivalent) (Contributed by Stefan O'Rear, 24-Feb-2015.) |
Ref | Expression |
---|---|
islinds4.j | ⊢ 𝐽 = (LBasis‘𝑊) |
Ref | Expression |
---|---|
islinds4 | ⊢ (𝑊 ∈ LVec → (𝑌 ∈ (LIndS‘𝑊) ↔ ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 468 | . . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) → 𝑊 ∈ LVec) | |
2 | eqid 2771 | . . . . . 6 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
3 | 2 | linds1 20366 | . . . . 5 ⊢ (𝑌 ∈ (LIndS‘𝑊) → 𝑌 ⊆ (Base‘𝑊)) |
4 | 3 | adantl 467 | . . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) → 𝑌 ⊆ (Base‘𝑊)) |
5 | lveclmod 19319 | . . . . . . 7 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | |
6 | 5 | ad2antrr 705 | . . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) ∧ 𝑥 ∈ 𝑌) → 𝑊 ∈ LMod) |
7 | eqid 2771 | . . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
8 | 7 | lvecdrng 19318 | . . . . . . . 8 ⊢ (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ DivRing) |
9 | drngnzr 19477 | . . . . . . . 8 ⊢ ((Scalar‘𝑊) ∈ DivRing → (Scalar‘𝑊) ∈ NzRing) | |
10 | 8, 9 | syl 17 | . . . . . . 7 ⊢ (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ NzRing) |
11 | 10 | ad2antrr 705 | . . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) ∧ 𝑥 ∈ 𝑌) → (Scalar‘𝑊) ∈ NzRing) |
12 | simplr 752 | . . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) ∧ 𝑥 ∈ 𝑌) → 𝑌 ∈ (LIndS‘𝑊)) | |
13 | simpr 471 | . . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑌) | |
14 | eqid 2771 | . . . . . . 7 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊) | |
15 | 14, 7 | lindsind2 20375 | . . . . . 6 ⊢ (((𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NzRing) ∧ 𝑌 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝑌) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝑌 ∖ {𝑥}))) |
16 | 6, 11, 12, 13, 15 | syl211anc 1482 | . . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) ∧ 𝑥 ∈ 𝑌) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝑌 ∖ {𝑥}))) |
17 | 16 | ralrimiva 3115 | . . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) → ∀𝑥 ∈ 𝑌 ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝑌 ∖ {𝑥}))) |
18 | islinds4.j | . . . . 5 ⊢ 𝐽 = (LBasis‘𝑊) | |
19 | 18, 2, 14 | lbsext 19378 | . . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝑌 ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ 𝑌 ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝑌 ∖ {𝑥}))) → ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏) |
20 | 1, 4, 17, 19 | syl3anc 1476 | . . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝑌 ∈ (LIndS‘𝑊)) → ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏) |
21 | 20 | ex 397 | . 2 ⊢ (𝑊 ∈ LVec → (𝑌 ∈ (LIndS‘𝑊) → ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏)) |
22 | 5 | ad2antrr 705 | . . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝑏 ∈ 𝐽) ∧ 𝑌 ⊆ 𝑏) → 𝑊 ∈ LMod) |
23 | 18 | lbslinds 20389 | . . . . . . 7 ⊢ 𝐽 ⊆ (LIndS‘𝑊) |
24 | 23 | sseli 3748 | . . . . . 6 ⊢ (𝑏 ∈ 𝐽 → 𝑏 ∈ (LIndS‘𝑊)) |
25 | 24 | ad2antlr 706 | . . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝑏 ∈ 𝐽) ∧ 𝑌 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑊)) |
26 | simpr 471 | . . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝑏 ∈ 𝐽) ∧ 𝑌 ⊆ 𝑏) → 𝑌 ⊆ 𝑏) | |
27 | lindsss 20380 | . . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑊) ∧ 𝑌 ⊆ 𝑏) → 𝑌 ∈ (LIndS‘𝑊)) | |
28 | 22, 25, 26, 27 | syl3anc 1476 | . . . 4 ⊢ (((𝑊 ∈ LVec ∧ 𝑏 ∈ 𝐽) ∧ 𝑌 ⊆ 𝑏) → 𝑌 ∈ (LIndS‘𝑊)) |
29 | 28 | ex 397 | . . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝑏 ∈ 𝐽) → (𝑌 ⊆ 𝑏 → 𝑌 ∈ (LIndS‘𝑊))) |
30 | 29 | rexlimdva 3179 | . 2 ⊢ (𝑊 ∈ LVec → (∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏 → 𝑌 ∈ (LIndS‘𝑊))) |
31 | 21, 30 | impbid 202 | 1 ⊢ (𝑊 ∈ LVec → (𝑌 ∈ (LIndS‘𝑊) ↔ ∃𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ∀wral 3061 ∃wrex 3062 ∖ cdif 3720 ⊆ wss 3723 {csn 4317 ‘cfv 6030 Basecbs 16064 Scalarcsca 16152 DivRingcdr 18957 LModclmod 19073 LSpanclspn 19184 LBasisclbs 19287 LVecclvec 19315 NzRingcnzr 19472 LIndSclinds 20361 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7100 ax-ac2 9491 ax-cnex 10198 ax-resscn 10199 ax-1cn 10200 ax-icn 10201 ax-addcl 10202 ax-addrcl 10203 ax-mulcl 10204 ax-mulrcl 10205 ax-mulcom 10206 ax-addass 10207 ax-mulass 10208 ax-distr 10209 ax-i2m1 10210 ax-1ne0 10211 ax-1rid 10212 ax-rnegex 10213 ax-rrecex 10214 ax-cnre 10215 ax-pre-lttri 10216 ax-pre-lttrn 10217 ax-pre-ltadd 10218 ax-pre-mulgt0 10219 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-isom 6039 df-riota 6757 df-ov 6799 df-oprab 6800 df-mpt2 6801 df-rpss 7088 df-om 7217 df-1st 7319 df-2nd 7320 df-tpos 7508 df-wrecs 7563 df-recs 7625 df-rdg 7663 df-1o 7717 df-oadd 7721 df-er 7900 df-en 8114 df-dom 8115 df-sdom 8116 df-fin 8117 df-card 8969 df-ac 9143 df-cda 9196 df-pnf 10282 df-mnf 10283 df-xr 10284 df-ltxr 10285 df-le 10286 df-sub 10474 df-neg 10475 df-nn 11227 df-2 11285 df-3 11286 df-ndx 16067 df-slot 16068 df-base 16070 df-sets 16071 df-ress 16072 df-plusg 16162 df-mulr 16163 df-0g 16310 df-mgm 17450 df-sgrp 17492 df-mnd 17503 df-grp 17633 df-minusg 17634 df-sbg 17635 df-cmn 18402 df-abl 18403 df-mgp 18698 df-ur 18710 df-ring 18757 df-oppr 18831 df-dvdsr 18849 df-unit 18850 df-invr 18880 df-drng 18959 df-lmod 19075 df-lss 19143 df-lsp 19185 df-lbs 19288 df-lvec 19316 df-nzr 19473 df-lindf 20362 df-linds 20363 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |