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

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 ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
Assertion dsmmbase ( 𝑅 ∈ 𝑉 → 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 dsmmval.b ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
2 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
3 1 ssrab3 ⊢ 𝐵 ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) )
4 eqid ⊢ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 )
5 eqid ⊢ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
6 4 5 ressbas2 ⊢ ( 𝐵 ⊆ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) → 𝐵 = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) ) )
7 3 6 ax-mp ⊢ 𝐵 = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
8 1 dsmmval ⊢ ( 𝑅 ∈ V → ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) )
9 8 fveq2d ⊢ ( 𝑅 ∈ V → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) = ( Base ‘ ( ( 𝑆 Xs 𝑅 ) ↾s 𝐵 ) ) )
10 7 9 eqtr4id ⊢ ( 𝑅 ∈ V → 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
11 2 10 syl ⊢ ( 𝑅 ∈ 𝑉 → 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )