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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin ) → ( 𝑆 ⊕m 𝑅 ) = ( 𝑆 Xs 𝑅 ) )