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 ⊢ A = subringAlg ⁡ R ⁡ V
sraring.2 ⊢ B = Base R
Assertion sraring ⊢ R ∈ Ring ∧ V ⊆ B → A ∈ Ring

Proof

Step Hyp Ref Expression
1 sraring.1 ⊢ A = subringAlg ⁡ R ⁡ V
2 sraring.2 ⊢ B = Base R
3 2 a1i ⊢ V ⊆ B → B = Base R
4 1 a1i ⊢ V ⊆ B → A = subringAlg ⁡ R ⁡ V
5 id ⊢ V ⊆ B → V ⊆ B
6 5 2 sseqtrdi ⊢ V ⊆ B → V ⊆ Base R
7 4 6 srabase ⊢ V ⊆ B → Base R = Base A
8 2 7 eqtrid ⊢ V ⊆ B → B = Base A
9 4 6 sraaddg ⊢ V ⊆ B → + R = + A
10 9 oveqdr ⊢ V ⊆ B ∧ x ∈ B ∧ y ∈ B → x + R y = x + A y
11 4 6 sramulr ⊢ V ⊆ B → ⋅ R = ⋅ A
12 11 oveqdr ⊢ V ⊆ B ∧ x ∈ B ∧ y ∈ B → x ⋅ R y = x ⋅ A y
13 3 8 10 12 ringpropd ⊢ V ⊆ B → R ∈ Ring ↔ A ∈ Ring
14 13 biimpac ⊢ R ∈ Ring ∧ V ⊆ B → A ∈ Ring