Description: The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rgspnval.r | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) | |
rgspnval.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) ) | ||
rgspnval.ss | ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) | ||
rgspnval.n | ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) ) | ||
rgspnval.sp | ⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) ) | ||
Assertion | rgspnssid | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rgspnval.r | ⊢ ( 𝜑 → 𝑅 ∈ Ring ) | |
2 | rgspnval.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) ) | |
3 | rgspnval.ss | ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) | |
4 | rgspnval.n | ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) ) | |
5 | rgspnval.sp | ⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) ) | |
6 | ssintub | ⊢ 𝐴 ⊆ ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } | |
7 | 1 2 3 4 5 | rgspnval | ⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ) |
8 | 6 7 | sseqtrrid | ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 ) |