qusdimsum

Description: Let W be a vector space, and let X be a subspace. Then the dimension of W is the sum of the dimension of X and the dimension of the quotient space of X . First part of theorem 5.3 in Lang p. 141. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypotheses	qusdimsum.x	$⊢ X = W ↾_{𝑠} U$
	qusdimsum.y	$⊢ Y = W /_{𝑠} (W ~_{QG} U)$
Assertion	qusdimsum	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (W) = \dim (X) +_{𝑒} \dim (Y)$

Proof

Step	Hyp	Ref	Expression
1		qusdimsum.x	$⊢ X = W ↾_{𝑠} U$
2		qusdimsum.y	$⊢ Y = W /_{𝑠} (W ~_{QG} U)$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4		lveclmod	$⊢ W \in LVec \to W \in LMod$
5	4	adantr	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W \in LMod$
6		simpr	$⊢ (W \in LVec \land U \in LSubSp (W)) \to U \in LSubSp (W)$
7		eqid	$⊢ (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) = (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))$
8	2 3 5 6 7	quslmhm	$⊢ (W \in LVec \land U \in LSubSp (W)) \to (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) \in (W LMHom Y)$
9		eqid	$⊢ 0_{Y} = 0_{Y}$
10		eqid	$⊢ W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}] = W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}]$
11		eqid	$⊢ Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) = Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))$
12	9 10 11	dimkerim	$⊢ (W \in LVec \land (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) \in (W LMHom Y)) \to \dim (W) = \dim (W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}]) +_{𝑒} \dim (Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)))$
13	8 12	syldan	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (W) = \dim (W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}]) +_{𝑒} \dim (Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)))$
14		eqid	$⊢ LSubSp (W) = LSubSp (W)$
15	14	lsssubg	$⊢ (W \in LMod \land U \in LSubSp (W)) \to U \in SubGrp (W)$
16	4 15	sylan	$⊢ (W \in LVec \land U \in LSubSp (W)) \to U \in SubGrp (W)$
17		lmodabl	$⊢ W \in LMod \to W \in Abel$
18	4 17	syl	$⊢ W \in LVec \to W \in Abel$
19	18	adantr	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W \in Abel$
20		ablnsg	$⊢ W \in Abel \to NrmSGrp (W) = SubGrp (W)$
21	19 20	syl	$⊢ (W \in LVec \land U \in LSubSp (W)) \to NrmSGrp (W) = SubGrp (W)$
22	16 21	eleqtrrd	$⊢ (W \in LVec \land U \in LSubSp (W)) \to U \in NrmSGrp (W)$
23	3 7 2 9	qusker	$⊢ U \in NrmSGrp (W) \to {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}] = U$
24	23	oveq2d	$⊢ U \in NrmSGrp (W) \to W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}] = W ↾_{𝑠} U$
25	22 24	syl	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}] = W ↾_{𝑠} U$
26	25 1	eqtr4di	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}] = X$
27	26	fveq2d	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}]) = \dim (X)$
28	2	a1i	$⊢ (W \in LVec \land U \in LSubSp (W)) \to Y = W /_{𝑠} (W ~_{QG} U)$
29	3	a1i	$⊢ (W \in LVec \land U \in LSubSp (W)) \to {Base}_{W} = {Base}_{W}$
30		ovexd	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W ~_{QG} U \in V$
31		simpl	$⊢ (W \in LVec \land U \in LSubSp (W)) \to W \in LVec$
32	28 29 7 30 31	quslem	$⊢ (W \in LVec \land U \in LSubSp (W)) \to (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) : {Base}_{W} \underset{onto}{⟶} {Base}_{W} / (W ~_{QG} U)$
33		forn	$⊢ (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) : {Base}_{W} \underset{onto}{⟶} {Base}_{W} / (W ~_{QG} U) \to ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) = {Base}_{W} / (W ~_{QG} U)$
34	32 33	syl	$⊢ (W \in LVec \land U \in LSubSp (W)) \to ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) = {Base}_{W} / (W ~_{QG} U)$
35	28 29 30 31	qusbas	$⊢ (W \in LVec \land U \in LSubSp (W)) \to {Base}_{W} / (W ~_{QG} U) = {Base}_{Y}$
36	34 35	eqtr2d	$⊢ (W \in LVec \land U \in LSubSp (W)) \to {Base}_{Y} = ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))$
37	36	oveq2d	$⊢ (W \in LVec \land U \in LSubSp (W)) \to Y ↾_{𝑠} {Base}_{Y} = Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))$
38	2	ovexi	$⊢ Y \in V$
39		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
40	39	ressid	$⊢ Y \in V \to Y ↾_{𝑠} {Base}_{Y} = Y$
41	38 40	ax-mp	$⊢ Y ↾_{𝑠} {Base}_{Y} = Y$
42	37 41	eqtr3di	$⊢ (W \in LVec \land U \in LSubSp (W)) \to Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U)) = Y$
43	42	fveq2d	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))) = \dim (Y)$
44	27 43	oveq12d	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (W ↾_{𝑠} {(x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))}^{-1} [\{0_{Y}\}]) +_{𝑒} \dim (Y ↾_{𝑠} ran (x \in {Base}_{W} ⟼ [x] (W ~_{QG} U))) = \dim (X) +_{𝑒} \dim (Y)$
45	13 44	eqtrd	$⊢ (W \in LVec \land U \in LSubSp (W)) \to \dim (W) = \dim (X) +_{𝑒} \dim (Y)$

Metamath Proof Explorer

Theorem qusdimsum

Proof