Theorem sraring

Description: Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023)

	Ref	Expression
Hypotheses	sraring.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
	sraring.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	sraring	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		sraring.1	⊢ 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 )
2		sraring.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
3	2	a1i	⊢ ( 𝑉 ⊆ 𝐵 → 𝐵 = ( Base ‘ 𝑅 ) )
4	1	a1i	⊢ ( 𝑉 ⊆ 𝐵 → 𝐴 = ( ( subringAlg ‘ 𝑅 ) ‘ 𝑉 ) )
5		id	⊢ ( 𝑉 ⊆ 𝐵 → 𝑉 ⊆ 𝐵 )
6	5 2	sseqtrdi	⊢ ( 𝑉 ⊆ 𝐵 → 𝑉 ⊆ ( Base ‘ 𝑅 ) )
7	4 6	srabase	⊢ ( 𝑉 ⊆ 𝐵 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐴 ) )
8	2 7	syl5eq	⊢ ( 𝑉 ⊆ 𝐵 → 𝐵 = ( Base ‘ 𝐴 ) )
9	4 6	sraaddg	⊢ ( 𝑉 ⊆ 𝐵 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝐴 ) )
10	9	oveqdr	⊢ ( ( 𝑉 ⊆ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) )
11	4 6	sramulr	⊢ ( 𝑉 ⊆ 𝐵 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐴 ) )
12	11	oveqdr	⊢ ( ( 𝑉 ⊆ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
13	3 8 10 12	ringpropd	⊢ ( 𝑉 ⊆ 𝐵 → ( 𝑅 ∈ Ring ↔ 𝐴 ∈ Ring ) )
14	13	biimpac	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑉 ⊆ 𝐵 ) → 𝐴 ∈ Ring )