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 ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion lssintcl ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lssintcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
3 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
4 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
5 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
6 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) )
7 1 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → 𝑆 = ( LSubSp ‘ 𝑊 ) )
8 intssuni2 ⊢ ( ( 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝑆 )
9 8 3adant1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝑆 )
10 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11 10 1 lssss ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ ( Base ‘ 𝑊 ) )
12 velpw ⊢ ( 𝑦 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑦 ⊆ ( Base ‘ 𝑊 ) )
13 11 12 sylibr ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝒫 ( Base ‘ 𝑊 ) )
14 13 ssriv ⊢ 𝑆 ⊆ 𝒫 ( Base ‘ 𝑊 )
15 sspwuni ⊢ ( 𝑆 ⊆ 𝒫 ( Base ‘ 𝑊 ) ↔ ∪ 𝑆 ⊆ ( Base ‘ 𝑊 ) )
16 14 15 mpbi ⊢ ∪ 𝑆 ⊆ ( Base ‘ 𝑊 )
17 9 16 sstrdi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ( Base ‘ 𝑊 ) )
18 simpl1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑊 ∈ LMod )
19 simp2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ 𝑆 )
20 19 sselda ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝑆 )
21 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
22 21 1 lss0cl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ 𝑦 )
23 18 20 22 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ∈ 𝐴 ) → ( 0g ‘ 𝑊 ) ∈ 𝑦 )
24 23 ralrimiva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∀ 𝑦 ∈ 𝐴 ( 0g ‘ 𝑊 ) ∈ 𝑦 )
25 fvex ⊢ ( 0g ‘ 𝑊 ) ∈ V
26 25 elint2 ⊢ ( ( 0g ‘ 𝑊 ) ∈ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 ( 0g ‘ 𝑊 ) ∈ 𝑦 )
27 24 26 sylibr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ( 0g ‘ 𝑊 ) ∈ ∩ 𝐴 )
28 27 ne0d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ≠ ∅ )
29 20 adantlr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝑆 )
30 simplr1 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31 simplr2 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑎 ∈ ∩ 𝐴 )
32 simpr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
33 elinti ⊢ ( 𝑎 ∈ ∩ 𝐴 → ( 𝑦 ∈ 𝐴 → 𝑎 ∈ 𝑦 ) )
34 31 32 33 sylc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑎 ∈ 𝑦 )
35 simplr3 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑏 ∈ ∩ 𝐴 )
36 elinti ⊢ ( 𝑏 ∈ ∩ 𝐴 → ( 𝑦 ∈ 𝐴 → 𝑏 ∈ 𝑦 ) )
37 35 32 36 sylc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑏 ∈ 𝑦 )
38 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
39 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
40 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
41 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
42 38 39 40 41 1 lsscl ⊢ ( ( 𝑦 ∈ 𝑆 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑦 ∧ 𝑏 ∈ 𝑦 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑦 )
43 29 30 34 37 42 syl13anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑦 )
44 43 ralrimiva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑦 )
45 ovex ⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ V
46 45 elint2 ⊢ ( ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ 𝑦 )
47 44 46 sylibr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ∩ 𝐴 ∧ 𝑏 ∈ ∩ 𝐴 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) 𝑏 ) ∈ ∩ 𝐴 )
48 2 3 4 5 6 7 17 28 47 islssd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑆 )