Metamath Proof Explorer

Theorem dsmmbase

Description: Base set of the module direct sum. (Contributed by Stefan O'Rear, 7-Jan-2015)

Ref Expression
Hypothesis dsmmval.b ⊢ B = f ∈ Base S ⨉ 𝑠 R | x ∈ dom ⁡ R | f ⁡ x ≠ 0 R ⁡ x ∈ Fin
Assertion dsmmbase ⊢ R ∈ V → B = Base S ⊕ m R

Proof

Step Hyp Ref Expression
1 dsmmval.b ⊢ B = f ∈ Base S ⨉ 𝑠 R | x ∈ dom ⁡ R | f ⁡ x ≠ 0 R ⁡ x ∈ Fin
2 elex ⊢ R ∈ V → R ∈ V
3 1 ssrab3 ⊢ B ⊆ Base S ⨉ 𝑠 R
4 eqid ⊢ S ⨉ 𝑠 R ↾ 𝑠 B = S ⨉ 𝑠 R ↾ 𝑠 B
5 eqid ⊢ Base S ⨉ 𝑠 R = Base S ⨉ 𝑠 R
6 4 5 ressbas2 ⊢ B ⊆ Base S ⨉ 𝑠 R → B = Base S ⨉ 𝑠 R ↾ 𝑠 B
7 3 6 ax-mp ⊢ B = Base S ⨉ 𝑠 R ↾ 𝑠 B
8 1 dsmmval ⊢ R ∈ V → S ⊕ m R = S ⨉ 𝑠 R ↾ 𝑠 B
9 8 fveq2d ⊢ R ∈ V → Base S ⊕ m R = Base S ⨉ 𝑠 R ↾ 𝑠 B
10 7 9 eqtr4id ⊢ R ∈ V → B = Base S ⊕ m R
11 2 10 syl ⊢ R ∈ V → B = Base S ⊕ m R