Metamath Proof Explorer

Theorem spansnji

Description: The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses spansnj.1 
|- A e. CH
spansnj.2 
|- B e. ~H
Assertion spansnji 
|- ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) )

Proof

Step Hyp Ref Expression
1 spansnj.1 
 |-  A e. CH
2 spansnj.2 
 |-  B e. ~H
3 1 chshii 
 |-  A e. SH
4 2 spansnchi 
 |-  ( span ` { B } ) e. CH
5 4 chshii 
 |-  ( span ` { B } ) e. SH
6 3 5 shjshsi 
 |-  ( A vH ( span ` { B } ) ) = ( _|_ ` ( _|_ ` ( A +H ( span ` { B } ) ) ) )
7 1 chssii 
 |-  A C_ ~H
8 1 choccli 
 |-  ( _|_ ` A ) e. CH
9 8 2 pjhclii 
 |-  ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H
10 snssi 
 |-  ( ( ( projh ` ( _|_ ` A ) ) ` B ) e. ~H -> { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ~H )
11 9 10 ax-mp 
 |-  { ( ( projh ` ( _|_ ` A ) ) ` B ) } C_ ~H
12 7 11 spanuni 
 |-  ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( ( span ` A ) +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
13 spanid 
 |-  ( A e. SH -> ( span ` A ) = A )
14 3 13 ax-mp 
 |-  ( span ` A ) = A
15 14 oveq1i 
 |-  ( ( span ` A ) +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
16 7 2 spansnpji 
 |-  A C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
17 9 spansnchi 
 |-  ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) e. CH
18 1 17 osumi 
 |-  ( A C_ ( _|_ ` ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) -> ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) )
19 16 18 ax-mp 
 |-  ( A +H ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
20 12 15 19 3eqtrri 
 |-  ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
21 1 2 spanunsni 
 |-  ( span ` ( A u. { B } ) ) = ( span ` ( A u. { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
22 20 21 eqtr4i 
 |-  ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) = ( span ` ( A u. { B } ) )
23 snssi 
 |-  ( B e. ~H -> { B } C_ ~H )
24 2 23 ax-mp 
 |-  { B } C_ ~H
25 7 24 spanuni 
 |-  ( span ` ( A u. { B } ) ) = ( ( span ` A ) +H ( span ` { B } ) )
26 14 oveq1i 
 |-  ( ( span ` A ) +H ( span ` { B } ) ) = ( A +H ( span ` { B } ) )
27 22 25 26 3eqtrri 
 |-  ( A +H ( span ` { B } ) ) = ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) )
28 1 17 chjcli 
 |-  ( A vH ( span ` { ( ( projh ` ( _|_ ` A ) ) ` B ) } ) ) e. CH
29 27 28 eqeltri 
 |-  ( A +H ( span ` { B } ) ) e. CH
30 29 ococi 
 |-  ( _|_ ` ( _|_ ` ( A +H ( span ` { B } ) ) ) ) = ( A +H ( span ` { B } ) )
31 6 30 eqtr2i 
 |-  ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) )