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

Metamath Proof Explorer

Theorem shsvs

Description: Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsvs 
|- ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( C -h D ) e. ( A +H B ) ) )

Proof

Step Hyp Ref Expression
1 shscl 
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) e. SH )
2 1 a1d 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( A +H B ) e. SH ) )
3 shsel1 
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. A -> C e. ( A +H B ) ) )
4 3 adantrd 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> C e. ( A +H B ) ) )
5 shsel2 
 |-  ( ( A e. SH /\ B e. SH ) -> ( D e. B -> D e. ( A +H B ) ) )
6 5 adantld 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> D e. ( A +H B ) ) )
7 2 4 6 3jcad 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( ( A +H B ) e. SH /\ C e. ( A +H B ) /\ D e. ( A +H B ) ) ) )
8 shsubcl 
 |-  ( ( ( A +H B ) e. SH /\ C e. ( A +H B ) /\ D e. ( A +H B ) ) -> ( C -h D ) e. ( A +H B ) )
9 7 8 syl6 
 |-  ( ( A e. SH /\ B e. SH ) -> ( ( C e. A /\ D e. B ) -> ( C -h D ) e. ( A +H B ) ) )