Metamath Proof Explorer

Theorem 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 ∈ LVec ∧ U ∈ LSubSp ⁡ W → 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 ∈ LVec → W ∈ LMod
5 4 adantr ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ∈ LMod
6 simpr ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → U ∈ LSubSp ⁡ W
7 eqid ⊢ x ∈ Base W ⟼ x W ~ QG U = x ∈ Base W ⟼ x W ~ QG U
8 2 3 5 6 7 quslmhm ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → x ∈ Base W ⟼ x W ~ QG U ∈ W LMHom Y
9 eqid ⊢ 0 Y = 0 Y
10 eqid ⊢ W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y = W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y
11 eqid ⊢ Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U = Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U
12 9 10 11 dimkerim ⊢ W ∈ LVec ∧ x ∈ Base W ⟼ x W ~ QG U ∈ W LMHom Y → dim ⁡ W = dim ⁡ W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y + 𝑒 dim ⁡ Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U
13 8 12 syldan ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → dim ⁡ W = dim ⁡ W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y + 𝑒 dim ⁡ Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U
14 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
15 14 lsssubg ⊢ W ∈ LMod ∧ U ∈ LSubSp ⁡ W → U ∈ SubGrp ⁡ W
16 4 15 sylan ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → U ∈ SubGrp ⁡ W
17 lmodabl ⊢ W ∈ LMod → W ∈ Abel
18 4 17 syl ⊢ W ∈ LVec → W ∈ Abel
19 18 adantr ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ∈ Abel
20 ablnsg ⊢ W ∈ Abel → NrmSGrp ⁡ W = SubGrp ⁡ W
21 19 20 syl ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → NrmSGrp ⁡ W = SubGrp ⁡ W
22 16 21 eleqtrrd ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → U ∈ NrmSGrp ⁡ W
23 3 7 2 9 qusker ⊢ U ∈ NrmSGrp ⁡ W → x ∈ Base W ⟼ x W ~ QG U -1 0 Y = U
24 23 oveq2d ⊢ U ∈ NrmSGrp ⁡ W → W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y = W ↾ 𝑠 U
25 22 24 syl ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y = W ↾ 𝑠 U
26 25 1 eqtr4di ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y = X
27 26 fveq2d ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → dim ⁡ W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y = dim ⁡ X
28 2 a1i ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Y = W / 𝑠 W ~ QG U
29 3 a1i ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Base W = Base W
30 ovexd ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ~ QG U ∈ V
31 simpl ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → W ∈ LVec
32 28 29 7 30 31 quslem ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → x ∈ Base W ⟼ x W ~ QG U : Base W ⟶ onto Base W / W ~ QG U
33 forn ⊢ x ∈ Base W ⟼ x W ~ QG U : Base W ⟶ onto Base W / W ~ QG U → ran ⁡ x ∈ Base W ⟼ x W ~ QG U = Base W / W ~ QG U
34 32 33 syl ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → ran ⁡ x ∈ Base W ⟼ x W ~ QG U = Base W / W ~ QG U
35 28 29 30 31 qusbas ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Base W / W ~ QG U = Base Y
36 34 35 eqtr2d ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Base Y = ran ⁡ x ∈ Base W ⟼ x W ~ QG U
37 36 oveq2d ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Y ↾ 𝑠 Base Y = Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U
38 2 ovexi ⊢ Y ∈ V
39 eqid ⊢ Base Y = Base Y
40 39 ressid ⊢ Y ∈ V → Y ↾ 𝑠 Base Y = Y
41 38 40 ax-mp ⊢ Y ↾ 𝑠 Base Y = Y
42 37 41 eqtr3di ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U = Y
43 42 fveq2d ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → dim ⁡ Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U = dim ⁡ Y
44 27 43 oveq12d ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → dim ⁡ W ↾ 𝑠 x ∈ Base W ⟼ x W ~ QG U -1 0 Y + 𝑒 dim ⁡ Y ↾ 𝑠 ran ⁡ x ∈ Base W ⟼ x W ~ QG U = dim ⁡ X + 𝑒 dim ⁡ Y
45 13 44 eqtrd ⊢ W ∈ LVec ∧ U ∈ LSubSp ⁡ W → dim ⁡ W = dim ⁡ X + 𝑒 dim ⁡ Y