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 𝑅 ) ) )