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 ‘ { 𝐵 } ) ) )