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 |`s U )
qusdimsum.y 
|- Y = ( W /s ( W ~QG U ) )
Assertion qusdimsum 
|- ( ( W e. LVec /\ U e. ( LSubSp ` W ) ) -> ( dim ` W ) = ( ( dim ` X ) +e ( dim ` Y ) ) )

Proof

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