Theorem spanun

Description: The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	spanun	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uneq1	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( 𝐴 ∪ 𝐵 ) = ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) )
2	1	fveq2d	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) ) )
3		fveq2	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( span ‘ 𝐴 ) = ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) )
4	3	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ 𝐵 ) ) )
5	2 4	eqeq12d	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) ↔ ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ 𝐵 ) ) ) )
6		uneq2	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) = ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) )
7	6	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) ) = ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) ) )
8		fveq2	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( span ‘ 𝐵 ) = ( span ‘ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) )
9	8	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ 𝐵 ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) ) )
10	7 9	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ 𝐵 ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ 𝐵 ) ) ↔ ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) ) ) )
11		sseq1	⊢ ( 𝐴 = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( 𝐴 ⊆ ℋ ↔ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ⊆ ℋ ) )
12		sseq1	⊢ ( ℋ = if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) → ( ℋ ⊆ ℋ ↔ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ⊆ ℋ ) )
13		ssid	⊢ ℋ ⊆ ℋ
14	11 12 13	elimhyp	⊢ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ⊆ ℋ
15		sseq1	⊢ ( 𝐵 = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( 𝐵 ⊆ ℋ ↔ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ⊆ ℋ ) )
16		sseq1	⊢ ( ℋ = if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) → ( ℋ ⊆ ℋ ↔ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ⊆ ℋ ) )
17	15 16 13	elimhyp	⊢ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ⊆ ℋ
18	14 17	spanuni	⊢ ( span ‘ ( if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ∪ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) ) = ( ( span ‘ if ( 𝐴 ⊆ ℋ , 𝐴 , ℋ ) ) +ℋ ( span ‘ if ( 𝐵 ⊆ ℋ , 𝐵 , ℋ ) ) )
19	5 10 18	dedth2h	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( span ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( span ‘ 𝐴 ) +ℋ ( span ‘ 𝐵 ) ) )