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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑉 ⊆ 𝐵 → 𝐵 = ( 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 )