Metamath Proof Explorer

Theorem lssintcl

Description: The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypothesis lssintcl.s 
|- S = ( LSubSp ` W )
Assertion lssintcl 
|- ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> |^| A e. S )

Proof

Step Hyp Ref Expression
1 lssintcl.s 
 |-  S = ( LSubSp ` W )
2 eqidd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( Scalar ` W ) = ( Scalar ` W ) )
3 eqidd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
4 eqidd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( Base ` W ) = ( Base ` W ) )
5 eqidd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( +g ` W ) = ( +g ` W ) )
6 eqidd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( .s ` W ) = ( .s ` W ) )
7 1 a1i 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> S = ( LSubSp ` W ) )
8 intssuni2 
 |-  ( ( A C_ S /\ A =/= (/) ) -> |^| A C_ U. S )
9 8 3adant1 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> |^| A C_ U. S )
10 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 10 1 lssss 
 |-  ( y e. S -> y C_ ( Base ` W ) )
12 velpw 
 |-  ( y e. ~P ( Base ` W ) <-> y C_ ( Base ` W ) )
13 11 12 sylibr 
 |-  ( y e. S -> y e. ~P ( Base ` W ) )
14 13 ssriv 
 |-  S C_ ~P ( Base ` W )
15 sspwuni 
 |-  ( S C_ ~P ( Base ` W ) <-> U. S C_ ( Base ` W ) )
16 14 15 mpbi 
 |-  U. S C_ ( Base ` W )
17 9 16 sstrdi 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> |^| A C_ ( Base ` W ) )
18 simpl1 
 |-  ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ y e. A ) -> W e. LMod )
19 simp2 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> A C_ S )
20 19 sselda 
 |-  ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ y e. A ) -> y e. S )
21 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
22 21 1 lss0cl 
 |-  ( ( W e. LMod /\ y e. S ) -> ( 0g ` W ) e. y )
23 18 20 22 syl2anc 
 |-  ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ y e. A ) -> ( 0g ` W ) e. y )
24 23 ralrimiva 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> A. y e. A ( 0g ` W ) e. y )
25 fvex 
 |-  ( 0g ` W ) e. _V
26 25 elint2 
 |-  ( ( 0g ` W ) e. |^| A <-> A. y e. A ( 0g ` W ) e. y )
27 24 26 sylibr 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> ( 0g ` W ) e. |^| A )
28 27 ne0d 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> |^| A =/= (/) )
29 20 adantlr 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> y e. S )
30 simplr1 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> x e. ( Base ` ( Scalar ` W ) ) )
31 simplr2 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> a e. |^| A )
32 simpr 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> y e. A )
33 elinti 
 |-  ( a e. |^| A -> ( y e. A -> a e. y ) )
34 31 32 33 sylc 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> a e. y )
35 simplr3 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> b e. |^| A )
36 elinti 
 |-  ( b e. |^| A -> ( y e. A -> b e. y ) )
37 35 32 36 sylc 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> b e. y )
38 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
39 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
40 eqid 
 |-  ( +g ` W ) = ( +g ` W )
41 eqid 
 |-  ( .s ` W ) = ( .s ` W )
42 38 39 40 41 1 lsscl 
 |-  ( ( y e. S /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. y /\ b e. y ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. y )
43 29 30 34 37 42 syl13anc 
 |-  ( ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) /\ y e. A ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. y )
44 43 ralrimiva 
 |-  ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) -> A. y e. A ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. y )
45 ovex 
 |-  ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. _V
46 45 elint2 
 |-  ( ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. |^| A <-> A. y e. A ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. y )
47 44 46 sylibr 
 |-  ( ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. |^| A /\ b e. |^| A ) ) -> ( ( x ( .s ` W ) a ) ( +g ` W ) b ) e. |^| A )
48 2 3 4 5 6 7 17 28 47 islssd 
 |-  ( ( W e. LMod /\ A C_ S /\ A =/= (/) ) -> |^| A e. S )