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	syl5eq	$⊢ 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		simpr	$⊢ (W \in AssAlg \land S \subseteq V) \to S \subseteq V$
27	15	elpw2	$⊢ S \in 𝒫 V \leftrightarrow S \subseteq V$
28	26 27	sylibr	$⊢ (W \in AssAlg \land S \subseteq V) \to S \in 𝒫 V$
29		assaring	$⊢ W \in AssAlg \to W \in Ring$
30	2	subrgid	$⊢ W \in Ring \to V \in SubRing (W)$
31	29 30	syl	$⊢ W \in AssAlg \to V \in SubRing (W)$
32		assalmod	$⊢ W \in AssAlg \to W \in LMod$
33	2 3	lss1	$⊢ W \in LMod \to V \in L$
34	32 33	syl	$⊢ W \in AssAlg \to V \in L$
35	31 34	elind	$⊢ W \in AssAlg \to V \in (SubRing (W) \cap L)$
36		sseq2	$⊢ t = V \to (S \subseteq t \leftrightarrow S \subseteq V)$
37	36	rspcev	$⊢ (V \in (SubRing (W) \cap L) \land S \subseteq V) \to \exists t \in (SubRing (W) \cap L) S \subseteq t$
38	35 37	sylan	$⊢ (W \in AssAlg \land S \subseteq V) \to \exists t \in (SubRing (W) \cap L) S \subseteq t$
39		intexrab	$⊢ \exists t \in (SubRing (W) \cap L) S \subseteq t \leftrightarrow ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
40	38 39	sylib	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
41	22 25 28 40	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\}$
42	21 41	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