Theorem rgspnid

Description: The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rgspnid.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	rgspnid.sr	⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
	rgspnid.sp	⊢ ( 𝜑 → 𝑆 = ( ( RingSpan ‘ 𝑅 ) ‘ 𝐴 ) )
Assertion	rgspnid	⊢ ( 𝜑 → 𝑆 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rgspnid.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
2		rgspnid.sr	⊢ ( 𝜑 → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
3		rgspnid.sp	⊢ ( 𝜑 → 𝑆 = ( ( RingSpan ‘ 𝑅 ) ‘ 𝐴 ) )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5	subrgss	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
8		eqidd	⊢ ( 𝜑 → ( RingSpan ‘ 𝑅 ) = ( RingSpan ‘ 𝑅 ) )
9		ssidd	⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 )
10	1 4 7 8 3 2 9	rgspnmin	⊢ ( 𝜑 → 𝑆 ⊆ 𝐴 )
11	1 4 7 8 3	rgspnssid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
12	10 11	eqssd	⊢ ( 𝜑 → 𝑆 = 𝐴 )