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