aspval

Description: Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	$⊢ A = AlgSpan (W)$
	aspval.v	$⊢ V = {Base}_{W}$
	aspval.l	$⊢ L = LSubSp (W)$
Assertion	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$

Proof

Step	Hyp	Ref	Expression
1		aspval.a	$⊢ A = AlgSpan (W)$
2		aspval.v	$⊢ V = {Base}_{W}$
3		aspval.l	$⊢ L = LSubSp (W)$
4		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
5	4 2	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
6	5	pweqd	$⊢ w = W \to 𝒫 {Base}_{w} = 𝒫 V$
7		fveq2	$⊢ w = W \to SubRing (w) = SubRing (W)$
8		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
9	8 3	eqtr4di	$⊢ w = W \to LSubSp (w) = L$
10	7 9	ineq12d	$⊢ w = W \to SubRing (w) \cap LSubSp (w) = SubRing (W) \cap L$
11	10	rabeqdv	$⊢ w = W \to \{t \in (SubRing (w) \cap LSubSp (w)) \| s \subseteq t\} = \{t \in (SubRing (W) \cap L) \| s \subseteq t\}$
12	11	inteqd	$⊢ w = W \to ⋂ \{t \in (SubRing (w) \cap LSubSp (w)) \| s \subseteq t\} = ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}$
13	6 12	mpteq12dv	$⊢ w = W \to (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in (SubRing (w) \cap LSubSp (w)) \| s \subseteq t\}) = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\})$
14		df-asp	$⊢ AlgSpan = (w \in AssAlg ⟼ (s \in 𝒫 {Base}_{w} ⟼ ⋂ \{t \in (SubRing (w) \cap LSubSp (w)) \| s \subseteq t\}))$
15	2	fvexi	$⊢ V \in V$
16	15	pwex	$⊢ 𝒫 V \in V$
17	16	mptex	$⊢ (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}) \in V$
18	13 14 17	fvmpt	$⊢ W \in AssAlg \to AlgSpan (W) = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\})$
19	1 18	eqtrid	$⊢ W \in AssAlg \to A = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\})$
20	19	fveq1d	$⊢ W \in AssAlg \to A (S) = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}) (S)$
21	20	adantr	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}) (S)$
22		eqid	$⊢ (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}) = (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\})$
23		sseq1	$⊢ s = S \to (s \subseteq t \leftrightarrow S \subseteq t)$
24	23	rabbidv	$⊢ s = S \to \{t \in (SubRing (W) \cap L) \| s \subseteq t\} = \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
25	24	inteqd	$⊢ s = S \to ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\} = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
26	15	elpw2	$⊢ S \in 𝒫 V \leftrightarrow S \subseteq V$
27	26	bilanri	$⊢ (W \in AssAlg \land S \subseteq V) \to S \in 𝒫 V$
28		assaring	$⊢ W \in AssAlg \to W \in Ring$
29	2	subrgid	$⊢ W \in Ring \to V \in SubRing (W)$
30	28 29	syl	$⊢ W \in AssAlg \to V \in SubRing (W)$
31		assalmod	$⊢ W \in AssAlg \to W \in LMod$
32	2 3	lss1	$⊢ W \in LMod \to V \in L$
33	31 32	syl	$⊢ W \in AssAlg \to V \in L$
34	30 33	elind	$⊢ W \in AssAlg \to V \in (SubRing (W) \cap L)$
35		sseq2	$⊢ t = V \to (S \subseteq t \leftrightarrow S \subseteq V)$
36	35	rspcev	$⊢ (V \in (SubRing (W) \cap L) \land S \subseteq V) \to \exists t \in (SubRing (W) \cap L) S \subseteq t$
37	34 36	sylan	$⊢ (W \in AssAlg \land S \subseteq V) \to \exists t \in (SubRing (W) \cap L) S \subseteq t$
38		intexrab	$⊢ \exists t \in (SubRing (W) \cap L) S \subseteq t \leftrightarrow ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
39	37 38	sylib	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
40	22 25 27 39	fvmptd3	$⊢ (W \in AssAlg \land S \subseteq V) \to (s \in 𝒫 V ⟼ ⋂ \{t \in (SubRing (W) \cap L) \| s \subseteq t\}) (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
41	21 40	eqtrd	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$

Metamath Proof Explorer

Theorem aspval

Proof