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

Metamath Proof Explorer

Theorem gsumsra

Description: The group sum in a subring algebra is the same as the ring's group sum. (Contributed by Thierry Arnoux, 28-May-2023)

Ref Expression
Hypotheses gsumsra.1 ⊢ A = subringAlg ⁡ R ⁡ B
gsumsra.2 ⊢ φ → F ∈ U
gsumsra.3 ⊢ φ → R ∈ V
gsumsra.4 ⊢ φ → A ∈ W
gsumsra.5 ⊢ φ → B ⊆ Base R
Assertion gsumsra ⊢ φ → ∑ R F = ∑ A F

Proof

Step Hyp Ref Expression
1 gsumsra.1 ⊢ A = subringAlg ⁡ R ⁡ B
2 gsumsra.2 ⊢ φ → F ∈ U
3 gsumsra.3 ⊢ φ → R ∈ V
4 gsumsra.4 ⊢ φ → A ∈ W
5 gsumsra.5 ⊢ φ → B ⊆ Base R
6 1 a1i ⊢ φ → A = subringAlg ⁡ R ⁡ B
7 6 5 srabase ⊢ φ → Base R = Base A
8 6 5 sraaddg ⊢ φ → + R = + A
9 2 3 4 7 8 gsumpropd ⊢ φ → ∑ R F = ∑ A F