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 ∧ 𝐴 ⊆ 𝑆 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑆 )