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 
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) ) )

Proof

Step Hyp Ref Expression
1 uneq1 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( A u. B ) = ( if ( A C_ ~H , A , ~H ) u. B ) )
2 1 fveq2d 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( span ` ( A u. B ) ) = ( span ` ( if ( A C_ ~H , A , ~H ) u. B ) ) )
3 fveq2 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( span ` A ) = ( span ` if ( A C_ ~H , A , ~H ) ) )
4 3 oveq1d 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( ( span ` A ) +H ( span ` B ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` B ) ) )
5 2 4 eqeq12d 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) ) <-> ( span ` ( if ( A C_ ~H , A , ~H ) u. B ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` B ) ) ) )
6 uneq2 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( if ( A C_ ~H , A , ~H ) u. B ) = ( if ( A C_ ~H , A , ~H ) u. if ( B C_ ~H , B , ~H ) ) )
7 6 fveq2d 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( span ` ( if ( A C_ ~H , A , ~H ) u. B ) ) = ( span ` ( if ( A C_ ~H , A , ~H ) u. if ( B C_ ~H , B , ~H ) ) ) )
8 fveq2 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( span ` B ) = ( span ` if ( B C_ ~H , B , ~H ) ) )
9 8 oveq2d 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` B ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` if ( B C_ ~H , B , ~H ) ) ) )
10 7 9 eqeq12d 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( ( span ` ( if ( A C_ ~H , A , ~H ) u. B ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` B ) ) <-> ( span ` ( if ( A C_ ~H , A , ~H ) u. if ( B C_ ~H , B , ~H ) ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` if ( B C_ ~H , B , ~H ) ) ) ) )
11 sseq1 
 |-  ( A = if ( A C_ ~H , A , ~H ) -> ( A C_ ~H <-> if ( A C_ ~H , A , ~H ) C_ ~H ) )
12 sseq1 
 |-  ( ~H = if ( A C_ ~H , A , ~H ) -> ( ~H C_ ~H <-> if ( A C_ ~H , A , ~H ) C_ ~H ) )
13 ssid 
 |-  ~H C_ ~H
14 11 12 13 elimhyp 
 |-  if ( A C_ ~H , A , ~H ) C_ ~H
15 sseq1 
 |-  ( B = if ( B C_ ~H , B , ~H ) -> ( B C_ ~H <-> if ( B C_ ~H , B , ~H ) C_ ~H ) )
16 sseq1 
 |-  ( ~H = if ( B C_ ~H , B , ~H ) -> ( ~H C_ ~H <-> if ( B C_ ~H , B , ~H ) C_ ~H ) )
17 15 16 13 elimhyp 
 |-  if ( B C_ ~H , B , ~H ) C_ ~H
18 14 17 spanuni 
 |-  ( span ` ( if ( A C_ ~H , A , ~H ) u. if ( B C_ ~H , B , ~H ) ) ) = ( ( span ` if ( A C_ ~H , A , ~H ) ) +H ( span ` if ( B C_ ~H , B , ~H ) ) )
19 5 10 18 dedth2h 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( span ` ( A u. B ) ) = ( ( span ` A ) +H ( span ` B ) ) )