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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
qusdimsum.y ⊢ 𝑌 = ( 𝑊 /s ( 𝑊 ~QG 𝑈 ) )
Assertion qusdimsum ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ 𝑊 ) = ( ( dim ‘ 𝑋 ) +𝑒 ( dim ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 qusdimsum.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 qusdimsum.y ⊢ 𝑌 = ( 𝑊 /s ( 𝑊 ~QG 𝑈 ) )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
5 4 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑊 ∈ LMod )
6 simpr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
7 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) )
8 2 3 5 6 7 quslmhm ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ∈ ( 𝑊 LMHom 𝑌 ) )
9 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
10 eqid ⊢ ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) = ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) )
11 eqid ⊢ ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) = ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) )
12 9 10 11 dimkerim ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ∈ ( 𝑊 LMHom 𝑌 ) ) → ( dim ‘ 𝑊 ) = ( ( dim ‘ ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) ) +𝑒 ( dim ‘ ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) ) ) )
13 8 12 syldan ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ 𝑊 ) = ( ( dim ‘ ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) ) +𝑒 ( dim ‘ ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) ) ) )
14 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
15 14 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
16 4 15 sylan ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
17 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
18 4 17 syl ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ Abel )
19 18 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑊 ∈ Abel )
20 ablnsg ⊢ ( 𝑊 ∈ Abel → ( NrmSGrp ‘ 𝑊 ) = ( SubGrp ‘ 𝑊 ) )
21 19 20 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( NrmSGrp ‘ 𝑊 ) = ( SubGrp ‘ 𝑊 ) )
22 16 21 eleqtrrd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑈 ∈ ( NrmSGrp ‘ 𝑊 ) )
23 3 7 2 9 qusker ⊢ ( 𝑈 ∈ ( NrmSGrp ‘ 𝑊 ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) = 𝑈 )
24 23 oveq2d ⊢ ( 𝑈 ∈ ( NrmSGrp ‘ 𝑊 ) → ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) = ( 𝑊 ↾s 𝑈 ) )
25 22 24 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) = ( 𝑊 ↾s 𝑈 ) )
26 25 1 eqtr4di ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) = 𝑋 )
27 26 fveq2d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) ) = ( dim ‘ 𝑋 ) )
28 2 a1i ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑌 = ( 𝑊 /s ( 𝑊 ~QG 𝑈 ) ) )
29 3 a1i ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
30 ovexd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑊 ~QG 𝑈 ) ∈ V )
31 simpl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑊 ∈ LVec )
32 28 29 7 30 31 quslem ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) : ( Base ‘ 𝑊 ) –onto→ ( ( Base ‘ 𝑊 ) / ( 𝑊 ~QG 𝑈 ) ) )
33 forn ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) : ( Base ‘ 𝑊 ) –onto→ ( ( Base ‘ 𝑊 ) / ( 𝑊 ~QG 𝑈 ) ) → ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) = ( ( Base ‘ 𝑊 ) / ( 𝑊 ~QG 𝑈 ) ) )
34 32 33 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) = ( ( Base ‘ 𝑊 ) / ( 𝑊 ~QG 𝑈 ) ) )
35 28 29 30 31 qusbas ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( Base ‘ 𝑊 ) / ( 𝑊 ~QG 𝑈 ) ) = ( Base ‘ 𝑌 ) )
36 34 35 eqtr2d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( Base ‘ 𝑌 ) = ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) )
37 36 oveq2d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑌 ↾s ( Base ‘ 𝑌 ) ) = ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) )
38 2 ovexi ⊢ 𝑌 ∈ V
39 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
40 39 ressid ⊢ ( 𝑌 ∈ V → ( 𝑌 ↾s ( Base ‘ 𝑌 ) ) = 𝑌 )
41 38 40 ax-mp ⊢ ( 𝑌 ↾s ( Base ‘ 𝑌 ) ) = 𝑌
42 37 41 eqtr3di ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) = 𝑌 )
43 42 fveq2d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) ) = ( dim ‘ 𝑌 ) )
44 27 43 oveq12d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( dim ‘ ( 𝑊 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) “ { ( 0g ‘ 𝑌 ) } ) ) ) +𝑒 ( dim ‘ ( 𝑌 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ [ 𝑥 ] ( 𝑊 ~QG 𝑈 ) ) ) ) ) = ( ( dim ‘ 𝑋 ) +𝑒 ( dim ‘ 𝑌 ) ) )
45 13 44 eqtrd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) → ( dim ‘ 𝑊 ) = ( ( dim ‘ 𝑋 ) +𝑒 ( dim ‘ 𝑌 ) ) )