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

Metamath Proof Explorer

Theorem spansnss

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnss 
|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )

Proof

Step Hyp Ref Expression
1 shel 
 |-  ( ( A e. SH /\ B e. A ) -> B e. ~H )
2 elspansn 
 |-  ( B e. ~H -> ( x e. ( span ` { B } ) <-> E. y e. CC x = ( y .h B ) ) )
3 1 2 syl 
 |-  ( ( A e. SH /\ B e. A ) -> ( x e. ( span ` { B } ) <-> E. y e. CC x = ( y .h B ) ) )
4 shmulcl 
 |-  ( ( A e. SH /\ y e. CC /\ B e. A ) -> ( y .h B ) e. A )
5 eleq1a 
 |-  ( ( y .h B ) e. A -> ( x = ( y .h B ) -> x e. A ) )
6 4 5 syl 
 |-  ( ( A e. SH /\ y e. CC /\ B e. A ) -> ( x = ( y .h B ) -> x e. A ) )
7 6 3exp 
 |-  ( A e. SH -> ( y e. CC -> ( B e. A -> ( x = ( y .h B ) -> x e. A ) ) ) )
8 7 com23 
 |-  ( A e. SH -> ( B e. A -> ( y e. CC -> ( x = ( y .h B ) -> x e. A ) ) ) )
9 8 imp 
 |-  ( ( A e. SH /\ B e. A ) -> ( y e. CC -> ( x = ( y .h B ) -> x e. A ) ) )
10 9 rexlimdv 
 |-  ( ( A e. SH /\ B e. A ) -> ( E. y e. CC x = ( y .h B ) -> x e. A ) )
11 3 10 sylbid 
 |-  ( ( A e. SH /\ B e. A ) -> ( x e. ( span ` { B } ) -> x e. A ) )
12 11 ssrdv 
 |-  ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )