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

Metamath Proof Explorer

Theorem sralmod0

Description: The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014)

Ref Expression
Hypotheses sralmod0.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
sralmod0.z ⊢ φ → 0 ˙ = 0 W
sralmod0.s ⊢ φ → S ⊆ Base W
Assertion sralmod0 ⊢ φ → 0 ˙ = 0 A

Proof

Step Hyp Ref Expression
1 sralmod0.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 sralmod0.z ⊢ φ → 0 ˙ = 0 W
3 sralmod0.s ⊢ φ → S ⊆ Base W
4 eqidd ⊢ φ → Base W = Base W
5 1 3 srabase ⊢ φ → Base W = Base A
6 1 3 sraaddg ⊢ φ → + W = + A
7 6 oveqdr ⊢ φ ∧ a ∈ Base W ∧ b ∈ Base W → a + W b = a + A b
8 4 5 7 grpidpropd ⊢ φ → 0 W = 0 A
9 2 8 eqtrd ⊢ φ → 0 ˙ = 0 A