Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
|- ( A = if ( A e. CH , A , ~H ) -> ( A +H ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) +H ( span ` { B } ) ) ) |
2 |
|
oveq1 |
|- ( A = if ( A e. CH , A , ~H ) -> ( A vH ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { B } ) ) ) |
3 |
1 2
|
eqeq12d |
|- ( A = if ( A e. CH , A , ~H ) -> ( ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) ) <-> ( if ( A e. CH , A , ~H ) +H ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { B } ) ) ) ) |
4 |
|
sneq |
|- ( B = if ( B e. ~H , B , 0h ) -> { B } = { if ( B e. ~H , B , 0h ) } ) |
5 |
4
|
fveq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( span ` { B } ) = ( span ` { if ( B e. ~H , B , 0h ) } ) ) |
6 |
5
|
oveq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , ~H ) +H ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) +H ( span ` { if ( B e. ~H , B , 0h ) } ) ) ) |
7 |
5
|
oveq2d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. CH , A , ~H ) vH ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { if ( B e. ~H , B , 0h ) } ) ) ) |
8 |
6 7
|
eqeq12d |
|- ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. CH , A , ~H ) +H ( span ` { B } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { B } ) ) <-> ( if ( A e. CH , A , ~H ) +H ( span ` { if ( B e. ~H , B , 0h ) } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { if ( B e. ~H , B , 0h ) } ) ) ) ) |
9 |
|
ifchhv |
|- if ( A e. CH , A , ~H ) e. CH |
10 |
|
ifhvhv0 |
|- if ( B e. ~H , B , 0h ) e. ~H |
11 |
9 10
|
spansnji |
|- ( if ( A e. CH , A , ~H ) +H ( span ` { if ( B e. ~H , B , 0h ) } ) ) = ( if ( A e. CH , A , ~H ) vH ( span ` { if ( B e. ~H , B , 0h ) } ) ) |
12 |
3 8 11
|
dedth2h |
|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) ) ) |