dimval - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dimval		Structured version Visualization version GIF version

Theorem dimval 34004

Description: The dimension of a vector space 𝐹 is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.)

**Hypothesis**
Ref	Expression
dimval.1	⊢ 𝐽 = (LBasis‘𝐹)

**Assertion**
Ref	Expression
dimval	⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆))

Proof of Theorem dimval Dummy variables 𝑡 𝑥 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3479	. . . 4 ⊢ (𝐹 ∈ LVec → 𝐹 ∈ V)
2		fveq2 6885	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = (LBasis‘𝐹))
3		dimval.1	. . . . . . . 8 ⊢ 𝐽 = (LBasis‘𝐹)
4	2, 3	eqtr4di 2819	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = 𝐽)
5	4	imaeq2d 6065	. . . . . 6 ⊢ (𝑓 = 𝐹 → (♯ “ (LBasis‘𝑓)) = (♯ “ 𝐽))
6	5	unieqd 4888	. . . . 5 ⊢ (𝑓 = 𝐹 → ∪ (♯ “ (LBasis‘𝑓)) = ∪ (♯ “ 𝐽))
7		df-dim 34003	. . . . 5 ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
8		hashf 14385	. . . . . . 7 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
9		ffun 6712	. . . . . . 7 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
10	3	fvexi 6899	. . . . . . . 8 ⊢ 𝐽 ∈ V
11	10	funimaex 6627	. . . . . . 7 ⊢ (Fun ♯ → (♯ “ 𝐽) ∈ V)
12	8, 9, 11	mp2b 10	. . . . . 6 ⊢ (♯ “ 𝐽) ∈ V
13	12	uniex 7745	. . . . 5 ⊢ ∪ (♯ “ 𝐽) ∈ V
14	6, 7, 13	fvmpt 6993	. . . 4 ⊢ (𝐹 ∈ V → (dim‘𝐹) = ∪ (♯ “ 𝐽))
15	1, 14	syl 18	. . 3 ⊢ (𝐹 ∈ LVec → (dim‘𝐹) = ∪ (♯ “ 𝐽))
16	15	adantr 486	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = ∪ (♯ “ 𝐽))
17	3	lvecdim 21296	. . . . . . . . . 10 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑡 ∈ 𝐽) → 𝑆 ≈ 𝑡)
18	17	ad4ant124 1192	. . . . . . . . 9 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑆 ≈ 𝑡)
19		hasheni 14395	. . . . . . . . 9 ⊢ (𝑆 ≈ 𝑡 → (♯‘𝑆) = (♯‘𝑡))
20	18, 19	syl 18	. . . . . . . 8 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → (♯‘𝑆) = (♯‘𝑡))
21	20	adantr 486	. . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑆) = (♯‘𝑡))
22		simpr 490	. . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑡) = 𝑥)
23	21, 22	eqtr2d 2802	. . . . . 6 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → 𝑥 = (♯‘𝑆))
24	8, 9	ax-mp 5	. . . . . . . 8 ⊢ Fun ♯
25		fvelima 6950	. . . . . . . 8 ⊢ ((Fun ♯ ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
26	24, 25	mpan 703	. . . . . . 7 ⊢ (𝑥 ∈ (♯ “ 𝐽) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
27	26	adantl 487	. . . . . 6 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
28	23, 27	r19.29a 3176	. . . . 5 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) → 𝑥 = (♯‘𝑆))
29	28	ralrimiva 3160	. . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆))
30		ne0i 4297	. . . . . . 7 ⊢ (𝑆 ∈ 𝐽 → 𝐽 ≠ ∅)
31	30	adantl 487	. . . . . 6 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → 𝐽 ≠ ∅)
32		ffn 6709	. . . . . . . . 9 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
33	8, 32	ax-mp 5	. . . . . . . 8 ⊢ ♯ Fn V
34		ssv 3964	. . . . . . . 8 ⊢ 𝐽 ⊆ V
35		fnimaeq0 6672	. . . . . . . 8 ⊢ ((♯ Fn V ∧ 𝐽 ⊆ V) → ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅))
36	33, 34, 35	mp2an 705	. . . . . . 7 ⊢ ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅)
37	36	necon3bii 3013	. . . . . 6 ⊢ ((♯ “ 𝐽) ≠ ∅ ↔ 𝐽 ≠ ∅)
38	31, 37	sylibr 237	. . . . 5 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (♯ “ 𝐽) ≠ ∅)
39		eqsn 4798	. . . . 5 ⊢ ((♯ “ 𝐽) ≠ ∅ → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆)))
40	38, 39	syl 18	. . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆)))
41	29, 40	mpbird 260	. . 3 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (♯ “ 𝐽) = {(♯‘𝑆)})
42	41	unieqd 4888	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∪ (♯ “ 𝐽) = ∪ {(♯‘𝑆)})
43		fvex 6898	. . . 4 ⊢ (♯‘𝑆) ∈ V
44	43	unisn 4894	. . 3 ⊢ ∪ {(♯‘𝑆)} = (♯‘𝑆)
45	44	a1i 11	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∪ {(♯‘𝑆)} = (♯‘𝑆))
46	16, 42, 45	3eqtrd 2805	1 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 Vcvv 3458 ∪ cun 3906 ⊆ wss 3908 ∅c0 4289 {csn 4592 ∪ cuni 4875 class class class wbr 5112 “ cima 5667 Fun wfun 6534 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 ≈ cen 8942 +∞cpnf 11250 ℕ₀cn0 12514 ♯chash 14377 LBasisclbs 21210 LVecclvec 21238 dimcldim 34002

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5241 ax-sep 5260 ax-nul 5272 ax-pow 5339 ax-pr 5407 ax-un 7738 ax-reg 9556 ax-inf2 9612 ax-ac2 10457 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4876 df-int 4916 df-iun 4961 df-iin 4962 df-br 5113 df-opab 5177 df-mpt 5196 df-tr 5222 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 df-tpos 8224 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-oi 9474 df-r1 9738 df-rank 9739 df-scott 9860 df-card 9936 df-acn 9939 df-ac 10111 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11453 df-neg 11454 df-nn 12244 df-2 12313 df-3 12314 df-4 12315 df-5 12316 df-6 12317 df-7 12318 df-8 12319 df-9 12320 df-n0 12515 df-xnn0 12588 df-z 12602 df-dec 12722 df-uz 12873 df-fz 13546 df-hash 14378 df-struct 17217 df-sets 17234 df-slot 17252 df-ndx 17264 df-base 17280 df-ress 17301 df-plusg 17333 df-mulr 17334 df-tset 17339 df-ple 17340 df-ocomp 17341 df-0g 17504 df-mre 17648 df-mrc 17649 df-mri 17650 df-acs 17651 df-proset 18360 df-drs 18361 df-poset 18379 df-ipo 18594 df-mgm 18708 df-sgrp 18787 df-mnd 18803 df-submnd 18852 df-grp 19013 df-minusg 19014 df-sbg 19015 df-subg 19199 df-cmn 19862 df-abl 19863 df-mgp 20227 df-rng 20241 df-ur 20274 df-ring 20327 df-oppr 20430 df-dvdsr 20450 df-unit 20451 df-invr 20481 df-drng 20844 df-lmod 20998 df-lss 21068 df-lsp 21108 df-lbs 21211 df-lvec 21239 df-dim 34003

This theorem is used by: dimcl 34006 lmimdim 34007 lvecdim0i 34009 lvecdim0 34010 lssdimle 34011 dimpropd 34012 rlmdim 34013 frlmdim 34014 lsatdim 34020 dimkerim 34030 fedgmul 34034 dimlssid 34035 extdg1id 34069 ccfldextdgrr 34075 fldextrspunlem1 34078 extdgfialglem1 34095

W3C validator