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