rgspnval

Description: Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014)

	Ref	Expression
Hypotheses	rgspnval.r	$⊢ φ \to R \in Ring$
	rgspnval.b	$⊢ φ \to B = {Base}_{R}$
	rgspnval.ss	$⊢ φ \to A \subseteq B$
	rgspnval.n	$⊢ φ \to N = RingSpan (R)$
	rgspnval.sp	$⊢ φ \to U = N (A)$
Assertion	rgspnval	$⊢ φ \to U = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	$⊢ φ \to R \in Ring$
2		rgspnval.b	$⊢ φ \to B = {Base}_{R}$
3		rgspnval.ss	$⊢ φ \to A \subseteq B$
4		rgspnval.n	$⊢ φ \to N = RingSpan (R)$
5		rgspnval.sp	$⊢ φ \to U = N (A)$
6	4	fveq1d	$⊢ φ \to N (A) = RingSpan (R) (A)$
7		elex	$⊢ R \in Ring \to R \in V$
8		fveq2	$⊢ a = R \to {Base}_{a} = {Base}_{R}$
9	8	pweqd	$⊢ a = R \to 𝒫 {Base}_{a} = 𝒫 {Base}_{R}$
10		fveq2	$⊢ a = R \to SubRing (a) = SubRing (R)$
11		rabeq	$⊢ SubRing (a) = SubRing (R) \to \{t \in SubRing (a) \| b \subseteq t\} = \{t \in SubRing (R) \| b \subseteq t\}$
12	10 11	syl	$⊢ a = R \to \{t \in SubRing (a) \| b \subseteq t\} = \{t \in SubRing (R) \| b \subseteq t\}$
13	12	inteqd	$⊢ a = R \to ⋂ \{t \in SubRing (a) \| b \subseteq t\} = ⋂ \{t \in SubRing (R) \| b \subseteq t\}$
14	9 13	mpteq12dv	$⊢ a = R \to (b \in 𝒫 {Base}_{a} ⟼ ⋂ \{t \in SubRing (a) \| b \subseteq t\}) = (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\})$
15		df-rgspn	$⊢ RingSpan = (a \in V ⟼ (b \in 𝒫 {Base}_{a} ⟼ ⋂ \{t \in SubRing (a) \| b \subseteq t\}))$
16		fvex	$⊢ {Base}_{R} \in V$
17	16	pwex	$⊢ 𝒫 {Base}_{R} \in V$
18	17	mptex	$⊢ (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\}) \in V$
19	14 15 18	fvmpt	$⊢ R \in V \to RingSpan (R) = (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\})$
20	1 7 19	3syl	$⊢ φ \to RingSpan (R) = (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\})$
21	20	fveq1d	$⊢ φ \to RingSpan (R) (A) = (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\}) (A)$
22		eqid	$⊢ (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\}) = (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\})$
23		sseq1	$⊢ b = A \to (b \subseteq t \leftrightarrow A \subseteq t)$
24	23	rabbidv	$⊢ b = A \to \{t \in SubRing (R) \| b \subseteq t\} = \{t \in SubRing (R) \| A \subseteq t\}$
25	24	inteqd	$⊢ b = A \to ⋂ \{t \in SubRing (R) \| b \subseteq t\} = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
26	3 2	sseqtrd	$⊢ φ \to A \subseteq {Base}_{R}$
27	16	elpw2	$⊢ A \in 𝒫 {Base}_{R} \leftrightarrow A \subseteq {Base}_{R}$
28	26 27	sylibr	$⊢ φ \to A \in 𝒫 {Base}_{R}$
29		eqid	$⊢ {Base}_{R} = {Base}_{R}$
30	29	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
31	1 30	syl	$⊢ φ \to {Base}_{R} \in SubRing (R)$
32	2 31	eqeltrd	$⊢ φ \to B \in SubRing (R)$
33		sseq2	$⊢ t = B \to (A \subseteq t \leftrightarrow A \subseteq B)$
34	33	rspcev	$⊢ (B \in SubRing (R) \land A \subseteq B) \to \exists t \in SubRing (R) A \subseteq t$
35	32 3 34	syl2anc	$⊢ φ \to \exists t \in SubRing (R) A \subseteq t$
36		intexrab	$⊢ \exists t \in SubRing (R) A \subseteq t \leftrightarrow ⋂ \{t \in SubRing (R) \| A \subseteq t\} \in V$
37	35 36	sylib	$⊢ φ \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \in V$
38	22 25 28 37	fvmptd3	$⊢ φ \to (b \in 𝒫 {Base}_{R} ⟼ ⋂ \{t \in SubRing (R) \| b \subseteq t\}) (A) = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
39	21 38	eqtrd	$⊢ φ \to RingSpan (R) (A) = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
40	5 6 39	3eqtrd	$⊢ φ \to U = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$

Metamath Proof Explorer

Theorem rgspnval

Proof