Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dimvalfi | Structured version Visualization version GIF version |
Description: The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 31792 does not depend on the axiom of choice, but it is limited to the case where the base 𝑆 is finite. (Contributed by Thierry Arnoux, 24-May-2023.) |
Ref | Expression |
---|---|
dimval.1 | ⊢ 𝐽 = (LBasis‘𝐹) |
Ref | Expression |
---|---|
dimvalfi | ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = (♯‘𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3459 | . . . 4 ⊢ (𝐹 ∈ LVec → 𝐹 ∈ V) | |
2 | fveq2 6811 | . . . . . . . 8 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = (LBasis‘𝐹)) | |
3 | dimval.1 | . . . . . . . 8 ⊢ 𝐽 = (LBasis‘𝐹) | |
4 | 2, 3 | eqtr4di 2795 | . . . . . . 7 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = 𝐽) |
5 | 4 | imaeq2d 5986 | . . . . . 6 ⊢ (𝑓 = 𝐹 → (♯ “ (LBasis‘𝑓)) = (♯ “ 𝐽)) |
6 | 5 | unieqd 4864 | . . . . 5 ⊢ (𝑓 = 𝐹 → ∪ (♯ “ (LBasis‘𝑓)) = ∪ (♯ “ 𝐽)) |
7 | df-dim 31791 | . . . . 5 ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | |
8 | hashf 14125 | . . . . . . 7 ⊢ ♯:V⟶(ℕ0 ∪ {+∞}) | |
9 | ffun 6640 | . . . . . . 7 ⊢ (♯:V⟶(ℕ0 ∪ {+∞}) → Fun ♯) | |
10 | 3 | fvexi 6825 | . . . . . . . 8 ⊢ 𝐽 ∈ V |
11 | 10 | funimaex 6558 | . . . . . . 7 ⊢ (Fun ♯ → (♯ “ 𝐽) ∈ V) |
12 | 8, 9, 11 | mp2b 10 | . . . . . 6 ⊢ (♯ “ 𝐽) ∈ V |
13 | 12 | uniex 7634 | . . . . 5 ⊢ ∪ (♯ “ 𝐽) ∈ V |
14 | 6, 7, 13 | fvmpt 6914 | . . . 4 ⊢ (𝐹 ∈ V → (dim‘𝐹) = ∪ (♯ “ 𝐽)) |
15 | 1, 14 | syl 17 | . . 3 ⊢ (𝐹 ∈ LVec → (dim‘𝐹) = ∪ (♯ “ 𝐽)) |
16 | 15 | 3ad2ant1 1132 | . 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = ∪ (♯ “ 𝐽)) |
17 | simpll1 1211 | . . . . . . . . . 10 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝐹 ∈ LVec) | |
18 | simpll2 1212 | . . . . . . . . . 10 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑆 ∈ 𝐽) | |
19 | simpr 485 | . . . . . . . . . 10 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑡 ∈ 𝐽) | |
20 | simpll3 1213 | . . . . . . . . . 10 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑆 ∈ Fin) | |
21 | 3, 17, 18, 19, 20 | lvecdimfi 31789 | . . . . . . . . 9 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑆 ≈ 𝑡) |
22 | hasheni 14135 | . . . . . . . . 9 ⊢ (𝑆 ≈ 𝑡 → (♯‘𝑆) = (♯‘𝑡)) | |
23 | 21, 22 | syl 17 | . . . . . . . 8 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → (♯‘𝑆) = (♯‘𝑡)) |
24 | 23 | adantr 481 | . . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑆) = (♯‘𝑡)) |
25 | simpr 485 | . . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑡) = 𝑥) | |
26 | 24, 25 | eqtr2d 2778 | . . . . . 6 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → 𝑥 = (♯‘𝑆)) |
27 | 8, 9 | ax-mp 5 | . . . . . . . 8 ⊢ Fun ♯ |
28 | fvelima 6874 | . . . . . . . 8 ⊢ ((Fun ♯ ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥) | |
29 | 27, 28 | mpan 687 | . . . . . . 7 ⊢ (𝑥 ∈ (♯ “ 𝐽) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥) |
30 | 29 | adantl 482 | . . . . . 6 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥) |
31 | 26, 30 | r19.29a 3156 | . . . . 5 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) ∧ 𝑥 ∈ (♯ “ 𝐽)) → 𝑥 = (♯‘𝑆)) |
32 | 31 | ralrimiva 3140 | . . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆)) |
33 | ne0i 4279 | . . . . . . 7 ⊢ (𝑆 ∈ 𝐽 → 𝐽 ≠ ∅) | |
34 | 33 | 3ad2ant2 1133 | . . . . . 6 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → 𝐽 ≠ ∅) |
35 | ffn 6637 | . . . . . . . . 9 ⊢ (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V) | |
36 | 8, 35 | ax-mp 5 | . . . . . . . 8 ⊢ ♯ Fn V |
37 | ssv 3955 | . . . . . . . 8 ⊢ 𝐽 ⊆ V | |
38 | fnimaeq0 6603 | . . . . . . . 8 ⊢ ((♯ Fn V ∧ 𝐽 ⊆ V) → ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅)) | |
39 | 36, 37, 38 | mp2an 689 | . . . . . . 7 ⊢ ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅) |
40 | 39 | necon3bii 2994 | . . . . . 6 ⊢ ((♯ “ 𝐽) ≠ ∅ ↔ 𝐽 ≠ ∅) |
41 | 34, 40 | sylibr 233 | . . . . 5 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (♯ “ 𝐽) ≠ ∅) |
42 | eqsn 4774 | . . . . 5 ⊢ ((♯ “ 𝐽) ≠ ∅ → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆))) | |
43 | 41, 42 | syl 17 | . . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆))) |
44 | 32, 43 | mpbird 256 | . . 3 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (♯ “ 𝐽) = {(♯‘𝑆)}) |
45 | 44 | unieqd 4864 | . 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → ∪ (♯ “ 𝐽) = ∪ {(♯‘𝑆)}) |
46 | fvex 6824 | . . . 4 ⊢ (♯‘𝑆) ∈ V | |
47 | 46 | unisn 4872 | . . 3 ⊢ ∪ {(♯‘𝑆)} = (♯‘𝑆) |
48 | 47 | a1i 11 | . 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → ∪ {(♯‘𝑆)} = (♯‘𝑆)) |
49 | 16, 45, 48 | 3eqtrd 2781 | 1 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin) → (dim‘𝐹) = (♯‘𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3441 ∪ cun 3895 ⊆ wss 3897 ∅c0 4267 {csn 4571 ∪ cuni 4850 class class class wbr 5087 “ cima 5610 Fun wfun 6459 Fn wfn 6460 ⟶wf 6461 ‘cfv 6465 ≈ cen 8778 Fincfn 8781 +∞cpnf 11079 ℕ0cn0 12306 ♯chash 14117 LBasisclbs 20408 LVecclvec 20436 dimcldim 31790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5224 ax-sep 5238 ax-nul 5245 ax-pow 5303 ax-pr 5367 ax-un 7628 ax-cnex 11000 ax-resscn 11001 ax-1cn 11002 ax-icn 11003 ax-addcl 11004 ax-addrcl 11005 ax-mulcl 11006 ax-mulrcl 11007 ax-mulcom 11008 ax-addass 11009 ax-mulass 11010 ax-distr 11011 ax-i2m1 11012 ax-1ne0 11013 ax-1rid 11014 ax-rnegex 11015 ax-rrecex 11016 ax-cnre 11017 ax-pre-lttri 11018 ax-pre-lttrn 11019 ax-pre-ltadd 11020 ax-pre-mulgt0 11021 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4268 df-if 4472 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4851 df-int 4893 df-iun 4939 df-iin 4940 df-br 5088 df-opab 5150 df-mpt 5171 df-tr 5205 df-id 5507 df-eprel 5513 df-po 5521 df-so 5522 df-fr 5562 df-we 5564 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-pred 6224 df-ord 6291 df-on 6292 df-lim 6293 df-suc 6294 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-riota 7272 df-ov 7318 df-oprab 7319 df-mpo 7320 df-om 7758 df-1st 7876 df-2nd 7877 df-tpos 8089 df-frecs 8144 df-wrecs 8175 df-recs 8249 df-rdg 8288 df-1o 8344 df-er 8546 df-en 8782 df-dom 8783 df-sdom 8784 df-fin 8785 df-card 9768 df-pnf 11084 df-mnf 11085 df-xr 11086 df-ltxr 11087 df-le 11088 df-sub 11280 df-neg 11281 df-nn 12047 df-2 12109 df-3 12110 df-n0 12307 df-xnn0 12379 df-z 12393 df-uz 12656 df-hash 14118 df-sets 16935 df-slot 16953 df-ndx 16965 df-base 16983 df-ress 17012 df-plusg 17045 df-mulr 17046 df-0g 17222 df-mre 17365 df-mrc 17366 df-mri 17367 df-acs 17368 df-mgm 18396 df-sgrp 18445 df-mnd 18456 df-submnd 18501 df-grp 18649 df-minusg 18650 df-sbg 18651 df-subg 18821 df-cmn 19456 df-abl 19457 df-mgp 19789 df-ur 19806 df-ring 19853 df-oppr 19930 df-dvdsr 19951 df-unit 19952 df-invr 19982 df-drng 20065 df-lmod 20197 df-lss 20266 df-lsp 20306 df-lbs 20409 df-lvec 20437 df-dim 31791 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |