Metamath Proof Explorer

Theorem islssd

Description: Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses islssd.f 
|- ( ph -> F = ( Scalar ` W ) )
islssd.b 
|- ( ph -> B = ( Base ` F ) )
islssd.v 
|- ( ph -> V = ( Base ` W ) )
islssd.p 
|- ( ph -> .+ = ( +g ` W ) )
islssd.t 
|- ( ph -> .x. = ( .s ` W ) )
islssd.s 
|- ( ph -> S = ( LSubSp ` W ) )
islssd.u 
|- ( ph -> U C_ V )
islssd.z 
|- ( ph -> U =/= (/) )
islssd.c 
|- ( ( ph /\ ( x e. B /\ a e. U /\ b e. U ) ) -> ( ( x .x. a ) .+ b ) e. U )
Assertion islssd 
|- ( ph -> U e. S )

Proof

Step Hyp Ref Expression
1 islssd.f 
 |-  ( ph -> F = ( Scalar ` W ) )
2 islssd.b 
 |-  ( ph -> B = ( Base ` F ) )
3 islssd.v 
 |-  ( ph -> V = ( Base ` W ) )
4 islssd.p 
 |-  ( ph -> .+ = ( +g ` W ) )
5 islssd.t 
 |-  ( ph -> .x. = ( .s ` W ) )
6 islssd.s 
 |-  ( ph -> S = ( LSubSp ` W ) )
7 islssd.u 
 |-  ( ph -> U C_ V )
8 islssd.z 
 |-  ( ph -> U =/= (/) )
9 islssd.c 
 |-  ( ( ph /\ ( x e. B /\ a e. U /\ b e. U ) ) -> ( ( x .x. a ) .+ b ) e. U )
10 7 3 sseqtrd 
 |-  ( ph -> U C_ ( Base ` W ) )
11 9 3exp2 
 |-  ( ph -> ( x e. B -> ( a e. U -> ( b e. U -> ( ( x .x. a ) .+ b ) e. U ) ) ) )
12 11 imp43 
 |-  ( ( ( ph /\ x e. B ) /\ ( a e. U /\ b e. U ) ) -> ( ( x .x. a ) .+ b ) e. U )
13 12 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U )
14 13 ex 
 |-  ( ph -> ( x e. B -> A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
15 1 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` W ) ) )
16 2 15 eqtrd 
 |-  ( ph -> B = ( Base ` ( Scalar ` W ) ) )
17 16 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` ( Scalar ` W ) ) ) )
18 4 oveqd 
 |-  ( ph -> ( ( x .x. a ) .+ b ) = ( ( x .x. a ) ( +g ` W ) b ) )
19 5 oveqd 
 |-  ( ph -> ( x .x. a ) = ( x ( .s ` W ) a ) )
20 19 oveq1d 
 |-  ( ph -> ( ( x .x. a ) ( +g ` W ) b ) = ( ( x ( .s ` W ) a ) ( +g ` W ) b ) )
21 18 20 eqtrd 
 |-  ( ph -> ( ( x .x. a ) .+ b ) = ( ( x ( .s ` W ) a ) ( +g ` W ) b ) )
22 21 eleq1d 
 |-  ( ph -> ( ( ( x .x. a ) .+ b ) e. U <-> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U ) )
23 22 2ralbidv 
 |-  ( ph -> ( A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U <-> A. a e. U A. b e. U ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U ) )
24 14 17 23 3imtr3d 
 |-  ( ph -> ( x e. ( Base ` ( Scalar ` W ) ) -> A. a e. U A. b e. U ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U ) )
25 24 ralrimiv 
 |-  ( ph -> A. x e. ( Base ` ( Scalar ` W ) ) A. a e. U A. b e. U ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U )
26 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
27 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
28 eqid 
 |-  ( Base ` W ) = ( Base ` W )
29 eqid 
 |-  ( +g ` W ) = ( +g ` W )
30 eqid 
 |-  ( .s ` W ) = ( .s ` W )
31 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
32 26 27 28 29 30 31 islss 
 |-  ( U e. ( LSubSp ` W ) <-> ( U C_ ( Base ` W ) /\ U =/= (/) /\ A. x e. ( Base ` ( Scalar ` W ) ) A. a e. U A. b e. U ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. U ) )
33 10 8 25 32 syl3anbrc 
 |-  ( ph -> U e. ( LSubSp ` W ) )
34 33 6 eleqtrrd 
 |-  ( ph -> U e. S )