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 33859

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 3474	. . . 4 ⊢ (𝐹 ∈ LVec → 𝐹 ∈ V)
2		fveq2 6863	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = (LBasis‘𝐹))
3		dimval.1	. . . . . . . 8 ⊢ 𝐽 = (LBasis‘𝐹)
4	2, 3	eqtr4di 2814	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (LBasis‘𝑓) = 𝐽)
5	4	imaeq2d 6046	. . . . . 6 ⊢ (𝑓 = 𝐹 → (♯ “ (LBasis‘𝑓)) = (♯ “ 𝐽))
6	5	unieqd 4877	. . . . 5 ⊢ (𝑓 = 𝐹 → ∪ (♯ “ (LBasis‘𝑓)) = ∪ (♯ “ 𝐽))
7		df-dim 33858	. . . . 5 ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓)))
8		hashf 14348	. . . . . . 7 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
9		ffun 6690	. . . . . . 7 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
10	3	fvexi 6877	. . . . . . . 8 ⊢ 𝐽 ∈ V
11	10	funimaex 6605	. . . . . . 7 ⊢ (Fun ♯ → (♯ “ 𝐽) ∈ V)
12	8, 9, 11	mp2b 10	. . . . . 6 ⊢ (♯ “ 𝐽) ∈ V
13	12	uniex 7720	. . . . 5 ⊢ ∪ (♯ “ 𝐽) ∈ V
14	6, 7, 13	fvmpt 6971	. . . 4 ⊢ (𝐹 ∈ V → (dim‘𝐹) = ∪ (♯ “ 𝐽))
15	1, 14	syl 17	. . 3 ⊢ (𝐹 ∈ LVec → (dim‘𝐹) = ∪ (♯ “ 𝐽))
16	15	adantr 484	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = ∪ (♯ “ 𝐽))
17	3	lvecdim 21207	. . . . . . . . . 10 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑡 ∈ 𝐽) → 𝑆 ≈ 𝑡)
18	17	ad4ant124 1186	. . . . . . . . 9 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → 𝑆 ≈ 𝑡)
19		hasheni 14358	. . . . . . . . 9 ⊢ (𝑆 ≈ 𝑡 → (♯‘𝑆) = (♯‘𝑡))
20	18, 19	syl 17	. . . . . . . 8 ⊢ ((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) → (♯‘𝑆) = (♯‘𝑡))
21	20	adantr 484	. . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑆) = (♯‘𝑡))
22		simpr 488	. . . . . . 7 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → (♯‘𝑡) = 𝑥)
23	21, 22	eqtr2d 2797	. . . . . 6 ⊢ (((((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) ∧ 𝑡 ∈ 𝐽) ∧ (♯‘𝑡) = 𝑥) → 𝑥 = (♯‘𝑆))
24	8, 9	ax-mp 5	. . . . . . . 8 ⊢ Fun ♯
25		fvelima 6928	. . . . . . . 8 ⊢ ((Fun ♯ ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
26	24, 25	mpan 700	. . . . . . 7 ⊢ (𝑥 ∈ (♯ “ 𝐽) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
27	26	adantl 485	. . . . . 6 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) → ∃𝑡 ∈ 𝐽 (♯‘𝑡) = 𝑥)
28	23, 27	r19.29a 3169	. . . . 5 ⊢ (((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) ∧ 𝑥 ∈ (♯ “ 𝐽)) → 𝑥 = (♯‘𝑆))
29	28	ralrimiva 3153	. . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆))
30		ne0i 4293	. . . . . . 7 ⊢ (𝑆 ∈ 𝐽 → 𝐽 ≠ ∅)
31	30	adantl 485	. . . . . 6 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → 𝐽 ≠ ∅)
32		ffn 6687	. . . . . . . . 9 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
33	8, 32	ax-mp 5	. . . . . . . 8 ⊢ ♯ Fn V
34		ssv 3960	. . . . . . . 8 ⊢ 𝐽 ⊆ V
35		fnimaeq0 6650	. . . . . . . 8 ⊢ ((♯ Fn V ∧ 𝐽 ⊆ V) → ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅))
36	33, 34, 35	mp2an 702	. . . . . . 7 ⊢ ((♯ “ 𝐽) = ∅ ↔ 𝐽 = ∅)
37	36	necon3bii 3008	. . . . . 6 ⊢ ((♯ “ 𝐽) ≠ ∅ ↔ 𝐽 ≠ ∅)
38	31, 37	sylibr 236	. . . . 5 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (♯ “ 𝐽) ≠ ∅)
39		eqsn 4786	. . . . 5 ⊢ ((♯ “ 𝐽) ≠ ∅ → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆)))
40	38, 39	syl 17	. . . 4 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ((♯ “ 𝐽) = {(♯‘𝑆)} ↔ ∀𝑥 ∈ (♯ “ 𝐽)𝑥 = (♯‘𝑆)))
41	29, 40	mpbird 259	. . 3 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (♯ “ 𝐽) = {(♯‘𝑆)})
42	41	unieqd 4877	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∪ (♯ “ 𝐽) = ∪ {(♯‘𝑆)})
43		fvex 6876	. . . 4 ⊢ (♯‘𝑆) ∈ V
44	43	unisn 4883	. . 3 ⊢ ∪ {(♯‘𝑆)} = (♯‘𝑆)
45	44	a1i 11	. 2 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → ∪ {(♯‘𝑆)} = (♯‘𝑆))
46	16, 42, 45	3eqtrd 2800	1 ⊢ ((𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽) → (dim‘𝐹) = (♯‘𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 Vcvv 3453 ∪ cun 3902 ⊆ wss 3904 ∅c0 4285 {csn 4581 ∪ cuni 4864 class class class wbr 5099 “ cima 5648 Fun wfun 6511 Fn wfn 6512 ⟶wf 6513 ‘cfv 6517 ≈ cen 8920 +∞cpnf 11210 ℕ₀cn0 12478 ♯chash 14340 LBasisclbs 21121 LVecclvec 21149 dimcldim 33857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-reg 9537 ax-inf2 9593 ax-ac2 10417 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-1st 7966 df-2nd 7967 df-tpos 8201 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8673 df-map 8805 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-oi 9455 df-r1 9719 df-rank 9720 df-card 9894 df-acn 9897 df-ac 10069 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-xnn0 12552 df-z 12566 df-dec 12686 df-uz 12837 df-fz 13510 df-hash 14341 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-mulr 17283 df-tset 17288 df-ple 17289 df-ocomp 17290 df-0g 17453 df-mre 17597 df-mrc 17598 df-mri 17599 df-acs 17600 df-proset 18309 df-drs 18310 df-poset 18328 df-ipo 18543 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-submnd 18801 df-grp 18961 df-minusg 18962 df-sbg 18963 df-subg 19148 df-cmn 19805 df-abl 19806 df-mgp 20170 df-rng 20182 df-ur 20211 df-ring 20264 df-oppr 20365 df-dvdsr 20385 df-unit 20386 df-invr 20416 df-drng 20760 df-lmod 20909 df-lss 20979 df-lsp 21019 df-lbs 21122 df-lvec 21150 df-dim 33858

This theorem is referenced by: dimcl 33861 lmimdim 33862 lvecdim0i 33864 lvecdim0 33865 lssdimle 33866 dimpropd 33867 rlmdim 33868 frlmdim 33869 lsatdim 33875 dimkerim 33885 fedgmul 33889 dimlssid 33890 extdg1id 33924 ccfldextdgrr 33930 fldextrspunlem1 33933 extdgfialglem1 33950

W3C validator