Theorem lssacs

Description: Submodules are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

	Ref	Expression
Hypotheses	lssacs.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lssacs.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssacs	⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ ( ACS ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		lssacs.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lssacs.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3	1 2	lssss	⊢ ( 𝑎 ∈ 𝑆 → 𝑎 ⊆ 𝐵 )
4	3	a1i	⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 → 𝑎 ⊆ 𝐵 ) )
5		inss2	⊢ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ⊆ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 }
6		ssrab2	⊢ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ⊆ 𝒫 𝐵
7	5 6	sstri	⊢ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ⊆ 𝒫 𝐵
8	7	sseli	⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ∈ 𝒫 𝐵 )
9	8	elpwid	⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ⊆ 𝐵 )
10	9	a1i	⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) → 𝑎 ⊆ 𝐵 ) )
11		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14	11 12 1 13 2	islss4	⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) )
15	14	adantr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) )
16		velpw	⊢ ( 𝑎 ∈ 𝒫 𝐵 ↔ 𝑎 ⊆ 𝐵 )
17		eleq2w	⊢ ( 𝑏 = 𝑎 → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
18	17	raleqbi1dv	⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
19	18	ralbidv	⊢ ( 𝑏 = 𝑎 → ( ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
20	19	elrab3	⊢ ( 𝑎 ∈ 𝒫 𝐵 → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
21	16 20	sylbir	⊢ ( 𝑎 ⊆ 𝐵 → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
22	21	adantl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) )
23	22	anbi2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑎 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑎 ) ) )
24	15 23	bitr4d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) )
25		elin	⊢ ( 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ↔ ( 𝑎 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑎 ∈ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) )
26	24 25	bitr4di	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ⊆ 𝐵 ) → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) )
27	26	ex	⊢ ( 𝑊 ∈ LMod → ( 𝑎 ⊆ 𝐵 → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) ) )
28	4 10 27	pm5.21ndd	⊢ ( 𝑊 ∈ LMod → ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ) )
29	28	eqrdv	⊢ ( 𝑊 ∈ LMod → 𝑆 = ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) )
30	1	fvexi	⊢ 𝐵 ∈ V
31		mreacs	⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
32	30 31	mp1i	⊢ ( 𝑊 ∈ LMod → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
33		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
34	1	subgacs	⊢ ( 𝑊 ∈ Grp → ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) )
35	33 34	syl	⊢ ( 𝑊 ∈ LMod → ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) )
36	1 11 13 12	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
37	36	3expb	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
38	37	ralrimivva	⊢ ( 𝑊 ∈ LMod → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 )
39		acsfn1c	⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝐵 ) → { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) )
40	30 38 39	sylancr	⊢ ( 𝑊 ∈ LMod → { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) )
41		mreincl	⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubGrp ‘ 𝑊 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ∈ ( ACS ‘ 𝐵 ) )
42	32 35 40 41	syl3anc	⊢ ( 𝑊 ∈ LMod → ( ( SubGrp ‘ 𝑊 ) ∩ { 𝑏 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑏 } ) ∈ ( ACS ‘ 𝐵 ) )
43	29 42	eqeltrd	⊢ ( 𝑊 ∈ LMod → 𝑆 ∈ ( ACS ‘ 𝐵 ) )