This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Subring algebras and ideals Subring algebras sraaddg
Description: 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) (Revised by AV , 29-Oct-2024)
Ref
Expression
Hypotheses
srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion
sraaddg ⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3
plusgid ⊢ +g = Slot ( +g ‘ ndx )
4
scandxnplusgndx ⊢ ( Scalar ‘ ndx ) ≠ ( +g ‘ ndx )
5
vscandxnplusgndx ⊢ ( · 𝑠 ‘ ndx ) ≠ ( +g ‘ ndx )
6
ipndxnplusgndx ⊢ ( · 𝑖 ‘ ndx ) ≠ ( +g ‘ ndx )
7
1 2 3 4 5 6
sralem ⊢ ( 𝜑 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝐴 ) )