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

Metamath Proof Explorer

Theorem spansnj

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

Ref Expression
Assertion spansnj ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { 𝐵 } ) ) )
2 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { 𝐵 } ) ) )
3 1 2 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) → ( ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { 𝐵 } ) ) ) )
4 sneq ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → { 𝐵 } = { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } )
5 4 fveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( span ‘ { 𝐵 } ) = ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) )
6 5 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) )
7 5 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) )
8 6 7 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { 𝐵 } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { 𝐵 } ) ) ↔ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) ) )
9 ifchhv ⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∈ Cℋ
10 ifhvhv0 ⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
11 9 10 spansnji ⊢ ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) +ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) ) = ( if ( 𝐴 ∈ Cℋ , 𝐴 , ℋ ) ∨ℋ ( span ‘ { if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) } ) )
12 3 8 11 dedth2h ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℋ ( span ‘ { 𝐵 } ) ) = ( 𝐴 ∨ℋ ( span ‘ { 𝐵 } ) ) )