Theorem dsmmfi

Description: For finite products, the direct sum is just the module product. See also the observation in Lang p. 129. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	dsmmfi	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 Xs 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) )
2	1	dsmmval2	⊢ ( 𝑆 ⊕m 𝑅 ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
3		eqid	⊢ ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs 𝑅 )
4		eqid	⊢ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
5		noel	⊢ ¬ 𝑓 ∈ ∅
6		reldmprds	⊢ Rel dom Xs
7	6	ovprc1	⊢ ( ¬ 𝑆 ∈ V → ( 𝑆 Xs 𝑅 ) = ∅ )
8	7	fveq2d	⊢ ( ¬ 𝑆 ∈ V → ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ( Base ‘ ∅ ) )
9		base0	⊢ ∅ = ( Base ‘ ∅ )
10	8 9	eqtr4di	⊢ ( ¬ 𝑆 ∈ V → ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ∅ )
11	10	eleq2d	⊢ ( ¬ 𝑆 ∈ V → ( 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ↔ 𝑓 ∈ ∅ ) )
12	5 11	mtbiri	⊢ ( ¬ 𝑆 ∈ V → ¬ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
13	12	con4i	⊢ ( 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) → 𝑆 ∈ V )
14	13	adantl	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑆 ∈ V )
15		simplr	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝐼 ∈ Fin )
16		simpll	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑅 Fn 𝐼 )
17		simpr	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
18	3 4 14 15 16 17	prdsbasfn	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑓 Fn 𝐼 )
19	18	fndmd	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → dom 𝑓 = 𝐼 )
20	19 15	eqeltrd	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → dom 𝑓 ∈ Fin )
21		difss	⊢ ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ⊆ 𝑓
22		dmss	⊢ ( ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ⊆ 𝑓 → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ⊆ dom 𝑓 )
23	21 22	ax-mp	⊢ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ⊆ dom 𝑓
24		ssfi	⊢ ( ( dom 𝑓 ∈ Fin ∧ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ⊆ dom 𝑓 ) → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin )
25	20 23 24	sylancl	⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin )
26	25	ralrimiva	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ∀ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin )
27		rabid2	⊢ ( ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } ↔ ∀ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin )
28	26 27	sylibr	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } )
29		eqid	⊢ { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin }
30	3 29	dsmmbas2	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
31	28 30	eqtr2d	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
32	31	oveq2d	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) = ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) )
33		ovex	⊢ ( 𝑆 Xs 𝑅 ) ∈ V
34	4	ressid	⊢ ( ( 𝑆 Xs 𝑅 ) ∈ V → ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) = ( 𝑆 Xs 𝑅 ) )
35	33 34	ax-mp	⊢ ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) = ( 𝑆 Xs 𝑅 )
36	32 35	eqtrdi	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( ( 𝑆 Xs 𝑅 ) ↾s ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) ) = ( 𝑆 Xs 𝑅 ) )
37	2 36	syl5eq	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 Xs 𝑅 ) )