Theorem aspval2

Description: The algebraic closure is the ring closure when the generating set is expanded to include all scalars.EDITORIAL : In light of this, is AlgSpan independently needed? (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypotheses	aspval2.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
	aspval2.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	aspval2.r	⊢ 𝑅 = ( mrCls ‘ ( SubRing ‘ 𝑊 ) )
	aspval2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	aspval2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ( 𝑅 ‘ ( ran 𝐶 ∪ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		aspval2.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval2.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
3		aspval2.r	⊢ 𝑅 = ( mrCls ‘ ( SubRing ‘ 𝑊 ) )
4		aspval2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
5		elin	⊢ ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ↔ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ) )
6	5	anbi1i	⊢ ( ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) )
7		anass	⊢ ( ( ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ 𝑥 ) ) )
8	6 7	bitri	⊢ ( ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ 𝑥 ) ) )
9		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
10	2 9	issubassa2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↔ ran 𝐶 ⊆ 𝑥 ) )
11	10	anbi1d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( SubRing ‘ 𝑊 ) ) → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( ran 𝐶 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥 ) ) )
12		unss	⊢ ( ( ran 𝐶 ⊆ 𝑥 ∧ 𝑆 ⊆ 𝑥 ) ↔ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 )
13	11 12	bitrdi	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( SubRing ‘ 𝑊 ) ) → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) )
14	13	pm5.32da	⊢ ( 𝑊 ∈ AssAlg → ( ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑆 ⊆ 𝑥 ) ) ↔ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) ) )
15	8 14	bitrid	⊢ ( 𝑊 ∈ AssAlg → ( ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) ↔ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) ) )
16	15	abbidv	⊢ ( 𝑊 ∈ AssAlg → { 𝑥 ∣ ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) } )
17	16	adantr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → { 𝑥 ∣ ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) } )
18		df-rab	⊢ { 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∧ 𝑆 ⊆ 𝑥 ) }
19		df-rab	⊢ { 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∣ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 ) }
20	17 18 19	3eqtr4g	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → { 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑥 } = { 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∣ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 } )
21	20	inteqd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ∩ { 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑥 } = ∩ { 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∣ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 } )
22	1 4 9	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑥 } )
23		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
24	4	subrgmre	⊢ ( 𝑊 ∈ Ring → ( SubRing ‘ 𝑊 ) ∈ ( Moore ‘ 𝑉 ) )
25	23 24	syl	⊢ ( 𝑊 ∈ AssAlg → ( SubRing ‘ 𝑊 ) ∈ ( Moore ‘ 𝑉 ) )
26		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
27		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
29	2 26 23 27 28 4	asclf	⊢ ( 𝑊 ∈ AssAlg → 𝐶 : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ 𝑉 )
30	29	frnd	⊢ ( 𝑊 ∈ AssAlg → ran 𝐶 ⊆ 𝑉 )
31	30	adantr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ran 𝐶 ⊆ 𝑉 )
32		simpr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
33	31 32	unssd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑉 )
34	3	mrcval	⊢ ( ( ( SubRing ‘ 𝑊 ) ∈ ( Moore ‘ 𝑉 ) ∧ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑉 ) → ( 𝑅 ‘ ( ran 𝐶 ∪ 𝑆 ) ) = ∩ { 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∣ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 } )
35	25 33 34	syl2an2r	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑅 ‘ ( ran 𝐶 ∪ 𝑆 ) ) = ∩ { 𝑥 ∈ ( SubRing ‘ 𝑊 ) ∣ ( ran 𝐶 ∪ 𝑆 ) ⊆ 𝑥 } )
36	21 22 35	3eqtr4d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ( 𝑅 ‘ ( ran 𝐶 ∪ 𝑆 ) ) )