This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ Cℋ
spansnj.2 ⊢ 𝐵 ∈ ℋ
Assertion spansnji ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 spansnj.1 ⊢ 𝐴 ∈ Cℋ
2 spansnj.2 ⊢ 𝐵 ∈ ℋ
3 1 chshii ⊢ 𝐴 ∈ Sℋ
4 2 spansnchi ⊢ ( span ‘ { 𝐵 } ) ∈ Cℋ
5 4 chshii ⊢ ( span ‘ { 𝐵 } ) ∈ Sℋ
6 3 5 shjshsi ⊢ ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) )
7 1 chssii ⊢ 𝐴 ⊆ ℋ
8 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
9 8 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ
10 snssi ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) ∈ ℋ → { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ )
11 9 10 ax-mp ⊢ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ⊆ ℋ
12 7 11 spanuni ⊢ ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
13 spanid ⊢ ( 𝐴 ∈ Sℋ → ( span ‘ 𝐴 ) = 𝐴 )
14 3 13 ax-mp ⊢ ( span ‘ 𝐴 ) = 𝐴
15 14 oveq1i ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
16 7 2 spansnpji ⊢ 𝐴 ⊆ ( ⊥ ‘ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
17 9 spansnchi ⊢ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ∈ Cℋ
18 1 17 osumi ⊢ ( 𝐴 ⊆ ( ⊥ ‘ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) → ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) )
19 16 18 ax-mp ⊢ ( 𝐴 +ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
20 12 15 19 3eqtrri ⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
21 1 2 spanunsni ⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( span ‘ ( 𝐴 ∪ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
22 20 21 eqtr4i ⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) = ( span ‘ ( 𝐴 ∪ { 𝐵 } ) )
23 snssi ⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
24 2 23 ax-mp ⊢ { 𝐵 } ⊆ ℋ
25 7 24 spanuni ⊢ ( span ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) )
26 14 oveq1i ⊢ ( ( span ‘ 𝐴 ) +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
27 22 25 26 3eqtrri ⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) )
28 1 17 chjcli ⊢ ( 𝐴 ∨ℋ ( span ‘ { ( ( projℎ ‘ ( ⊥ ‘ 𝐴 ) ) ‘ 𝐵 ) } ) ) ∈ Cℋ
29 27 28 eqeltri ⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ∈ Cℋ
30 29 ococi ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) ) ) = ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) )
31 6 30 eqtr2i ⊢ ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) )