This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )