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

Metamath Proof Explorer

Theorem sra1r

Description: The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023)

Ref Expression
Hypotheses sral1r.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
sral1r.1 ⊢ φ → 1 ˙ = 1 W
sral1r.s ⊢ φ → S ⊆ Base W
Assertion sra1r ⊢ φ → 1 ˙ = 1 A

Proof

Step Hyp Ref Expression
1 sral1r.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 sral1r.1 ⊢ φ → 1 ˙ = 1 W
3 sral1r.s ⊢ φ → S ⊆ Base W
4 eqidd ⊢ φ → Base W = Base W
5 1 3 srabase ⊢ φ → Base W = Base A
6 1 3 sramulr ⊢ φ → ⋅ W = ⋅ A
7 6 oveqdr ⊢ φ ∧ x ∈ Base W ∧ y ∈ Base W → x ⋅ W y = x ⋅ A y
8 4 5 7 rngidpropd ⊢ φ → 1 W = 1 A
9 2 8 eqtrd ⊢ φ → 1 ˙ = 1 A