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

Metamath Proof Explorer

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