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	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
	rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
Assertion	rgspnval	⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
2		rgspnval.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
3		rgspnval.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4		rgspnval.n	⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
5		rgspnval.sp	⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
6	4	fveq1d	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐴 ) = ( ( RingSpan ‘ 𝑅 ) ‘ 𝐴 ) )
7		elex	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ V )
8		fveq2	⊢ ( 𝑎 = 𝑅 → ( Base ‘ 𝑎 ) = ( Base ‘ 𝑅 ) )
9	8	pweqd	⊢ ( 𝑎 = 𝑅 → 𝒫 ( Base ‘ 𝑎 ) = 𝒫 ( Base ‘ 𝑅 ) )
10		fveq2	⊢ ( 𝑎 = 𝑅 → ( SubRing ‘ 𝑎 ) = ( SubRing ‘ 𝑅 ) )
11		rabeq	⊢ ( ( SubRing ‘ 𝑎 ) = ( SubRing ‘ 𝑅 ) → { 𝑡 ∈ ( SubRing ‘ 𝑎 ) ∣ 𝑏 ⊆ 𝑡 } = { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } )
12	10 11	syl	⊢ ( 𝑎 = 𝑅 → { 𝑡 ∈ ( SubRing ‘ 𝑎 ) ∣ 𝑏 ⊆ 𝑡 } = { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } )
13	12	inteqd	⊢ ( 𝑎 = 𝑅 → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑎 ) ∣ 𝑏 ⊆ 𝑡 } = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } )
14	9 13	mpteq12dv	⊢ ( 𝑎 = 𝑅 → ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑎 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑎 ) ∣ 𝑏 ⊆ 𝑡 } ) = ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) )
15		df-rgspn	⊢ RingSpan = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑎 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑎 ) ∣ 𝑏 ⊆ 𝑡 } ) )
16		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
17	16	pwex	⊢ 𝒫 ( Base ‘ 𝑅 ) ∈ V
18	17	mptex	⊢ ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) ∈ V
19	14 15 18	fvmpt	⊢ ( 𝑅 ∈ V → ( RingSpan ‘ 𝑅 ) = ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) )
20	1 7 19	3syl	⊢ ( 𝜑 → ( RingSpan ‘ 𝑅 ) = ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) )
21	20	fveq1d	⊢ ( 𝜑 → ( ( RingSpan ‘ 𝑅 ) ‘ 𝐴 ) = ( ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) ‘ 𝐴 ) )
22		eqid	⊢ ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) = ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } )
23		sseq1	⊢ ( 𝑏 = 𝐴 → ( 𝑏 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝑡 ) )
24	23	rabbidv	⊢ ( 𝑏 = 𝐴 → { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } = { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
25	24	inteqd	⊢ ( 𝑏 = 𝐴 → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
26	3 2	sseqtrd	⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
27	16	elpw2	⊢ ( 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) ↔ 𝐴 ⊆ ( Base ‘ 𝑅 ) )
28	26 27	sylibr	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ( Base ‘ 𝑅 ) )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30	29	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
31	1 30	syl	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
32	2 31	eqeltrd	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
33		sseq2	⊢ ( 𝑡 = 𝐵 → ( 𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝐵 ) )
34	33	rspcev	⊢ ( ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐴 ⊆ 𝐵 ) → ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 )
35	32 3 34	syl2anc	⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 )
36		intexrab	⊢ ( ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 ↔ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ∈ V )
37	35 36	sylib	⊢ ( 𝜑 → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ∈ V )
38	22 25 28 37	fvmptd3	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝒫 ( Base ‘ 𝑅 ) ↦ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝑏 ⊆ 𝑡 } ) ‘ 𝐴 ) = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
39	21 38	eqtrd	⊢ ( 𝜑 → ( ( RingSpan ‘ 𝑅 ) ‘ 𝐴 ) = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
40	5 6 39	3eqtrd	⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )

Metamath Proof Explorer

Theorem rgspnval

Proof