Metamath Proof Explorer


Theorem sraaddgOLD

Description: Obsolete proof of sraaddg as of 29-Oct-2024. Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses srapart.a φ A = subringAlg W S
srapart.s φ S Base W
Assertion sraaddgOLD φ + W = + A

Proof

Step Hyp Ref Expression
1 srapart.a φ A = subringAlg W S
2 srapart.s φ S Base W
3 df-plusg + 𝑔 = Slot 2
4 2nn 2
5 2lt5 2 < 5
6 5 orci 2 < 5 8 < 2
7 1 2 3 4 6 sralemOLD φ + W = + A