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	$⊢ A = AlgSpan (W)$
	aspval2.c	$⊢ C = algSc (W)$
	aspval2.r	$⊢ R = mrCls (SubRing (W))$
	aspval2.v	$⊢ V = {Base}_{W}$
Assertion	aspval2	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = R (ran C \cup S)$

Proof

Step	Hyp	Ref	Expression
1		aspval2.a	$⊢ A = AlgSpan (W)$
2		aspval2.c	$⊢ C = algSc (W)$
3		aspval2.r	$⊢ R = mrCls (SubRing (W))$
4		aspval2.v	$⊢ V = {Base}_{W}$
5		elin	$⊢ x \in (SubRing (W) \cap LSubSp (W)) \leftrightarrow (x \in SubRing (W) \land x \in LSubSp (W))$
6	5	anbi1i	$⊢ (x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x) \leftrightarrow ((x \in SubRing (W) \land x \in LSubSp (W)) \land S \subseteq x)$
7		anass	$⊢ ((x \in SubRing (W) \land x \in LSubSp (W)) \land S \subseteq x) \leftrightarrow (x \in SubRing (W) \land (x \in LSubSp (W) \land S \subseteq x))$
8	6 7	bitri	$⊢ (x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x) \leftrightarrow (x \in SubRing (W) \land (x \in LSubSp (W) \land S \subseteq x))$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	2 9	issubassa2	$⊢ (W \in AssAlg \land x \in SubRing (W)) \to (x \in LSubSp (W) \leftrightarrow ran C \subseteq x)$
11	10	anbi1d	$⊢ (W \in AssAlg \land x \in SubRing (W)) \to ((x \in LSubSp (W) \land S \subseteq x) \leftrightarrow (ran C \subseteq x \land S \subseteq x))$
12		unss	$⊢ (ran C \subseteq x \land S \subseteq x) \leftrightarrow ran C \cup S \subseteq x$
13	11 12	bitrdi	$⊢ (W \in AssAlg \land x \in SubRing (W)) \to ((x \in LSubSp (W) \land S \subseteq x) \leftrightarrow ran C \cup S \subseteq x)$
14	13	pm5.32da	$⊢ W \in AssAlg \to ((x \in SubRing (W) \land (x \in LSubSp (W) \land S \subseteq x)) \leftrightarrow (x \in SubRing (W) \land ran C \cup S \subseteq x))$
15	8 14	syl5bb	$⊢ W \in AssAlg \to ((x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x) \leftrightarrow (x \in SubRing (W) \land ran C \cup S \subseteq x))$
16	15	abbidv	$⊢ W \in AssAlg \to \{x \| (x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x)\} = \{x \| (x \in SubRing (W) \land ran C \cup S \subseteq x)\}$
17	16	adantr	$⊢ (W \in AssAlg \land S \subseteq V) \to \{x \| (x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x)\} = \{x \| (x \in SubRing (W) \land ran C \cup S \subseteq x)\}$
18		df-rab	$⊢ \{x \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq x\} = \{x \| (x \in (SubRing (W) \cap LSubSp (W)) \land S \subseteq x)\}$
19		df-rab	$⊢ \{x \in SubRing (W) \| ran C \cup S \subseteq x\} = \{x \| (x \in SubRing (W) \land ran C \cup S \subseteq x)\}$
20	17 18 19	3eqtr4g	$⊢ (W \in AssAlg \land S \subseteq V) \to \{x \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq x\} = \{x \in SubRing (W) \| ran C \cup S \subseteq x\}$
21	20	inteqd	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{x \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq x\} = ⋂ \{x \in SubRing (W) \| ran C \cup S \subseteq x\}$
22	1 4 9	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{x \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq x\}$
23		assaring	$⊢ W \in AssAlg \to W \in Ring$
24	4	subrgmre	$⊢ W \in Ring \to SubRing (W) \in Moore (V)$
25	23 24	syl	$⊢ W \in AssAlg \to SubRing (W) \in Moore (V)$
26		eqid	$⊢ Scalar (W) = Scalar (W)$
27		assalmod	$⊢ W \in AssAlg \to W \in LMod$
28		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
29	2 26 23 27 28 4	asclf	$⊢ W \in AssAlg \to C : {Base}_{Scalar (W)} ⟶ V$
30	29	frnd	$⊢ W \in AssAlg \to ran C \subseteq V$
31	30	adantr	$⊢ (W \in AssAlg \land S \subseteq V) \to ran C \subseteq V$
32		simpr	$⊢ (W \in AssAlg \land S \subseteq V) \to S \subseteq V$
33	31 32	unssd	$⊢ (W \in AssAlg \land S \subseteq V) \to ran C \cup S \subseteq V$
34	3	mrcval	$⊢ (SubRing (W) \in Moore (V) \land ran C \cup S \subseteq V) \to R (ran C \cup S) = ⋂ \{x \in SubRing (W) \| ran C \cup S \subseteq x\}$
35	25 33 34	syl2an2r	$⊢ (W \in AssAlg \land S \subseteq V) \to R (ran C \cup S) = ⋂ \{x \in SubRing (W) \| ran C \cup S \subseteq x\}$
36	21 22 35	3eqtr4d	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = R (ran C \cup S)$

Metamath Proof Explorer

Theorem aspval2

Proof