Metamath Proof Explorer

Theorem dsmmbas2

Description: Base set of the direct sum module using the fndmin abbreviation. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses dsmmbas2.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
dsmmbas2.b ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ 𝑃 ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin }
Assertion dsmmbas2 ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 dsmmbas2.p ⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2 dsmmbas2.b ⊢ 𝐵 = { 𝑓 ∈ ( Base ‘ 𝑃 ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin }
3 1 fveq2i ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
4 3 rabeqi ⊢ { 𝑓 ∈ ( Base ‘ 𝑃 ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin }
5 simpll ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑅 Fn 𝐼 )
6 fvco2 ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
7 5 6 sylan ⊢ ( ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
8 7 neeq2d ⊢ ( ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) ≠ ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
9 8 rabbidva ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) } = { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
10 eqid ⊢ ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs 𝑅 )
11 eqid ⊢ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
12 reldmprds ⊢ Rel dom Xs
13 10 11 12 strov2rcl ⊢ ( 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) → 𝑆 ∈ V )
14 13 adantl ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑆 ∈ V )
15 simplr ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝐼 ∈ 𝑉 )
16 simpr ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) )
17 10 11 14 15 5 16 prdsbasfn ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → 𝑓 Fn 𝐼 )
18 fn0g ⊢ 0g Fn V
19 dffn2 ⊢ ( 0g Fn V ↔ 0g : V ⟶ V )
20 18 19 mpbi ⊢ 0g : V ⟶ V
21 dffn2 ⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 : 𝐼 ⟶ V )
22 21 biimpi ⊢ ( 𝑅 Fn 𝐼 → 𝑅 : 𝐼 ⟶ V )
23 fco ⊢ ( ( 0g : V ⟶ V ∧ 𝑅 : 𝐼 ⟶ V ) → ( 0g ∘ 𝑅 ) : 𝐼 ⟶ V )
24 20 22 23 sylancr ⊢ ( 𝑅 Fn 𝐼 → ( 0g ∘ 𝑅 ) : 𝐼 ⟶ V )
25 24 ffnd ⊢ ( 𝑅 Fn 𝐼 → ( 0g ∘ 𝑅 ) Fn 𝐼 )
26 5 25 syl ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → ( 0g ∘ 𝑅 ) Fn 𝐼 )
27 fndmdif ⊢ ( ( 𝑓 Fn 𝐼 ∧ ( 0g ∘ 𝑅 ) Fn 𝐼 ) → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) } )
28 17 26 27 syl2anc ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) = { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) } )
29 fndm ⊢ ( 𝑅 Fn 𝐼 → dom 𝑅 = 𝐼 )
30 29 rabeqdv ⊢ ( 𝑅 Fn 𝐼 → { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } = { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
31 5 30 syl ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } = { 𝑥 ∈ 𝐼 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
32 9 28 31 3eqtr4d ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) = { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } )
33 32 eleq1d ⊢ ( ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ) → ( dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin ↔ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin ) )
34 33 rabbidva ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } )
35 4 34 syl5eq ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( Base ‘ 𝑃 ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } )
36 fnex ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → 𝑅 ∈ V )
37 eqid ⊢ { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin }
38 37 dsmmbase ⊢ ( 𝑅 ∈ V → { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
39 36 38 syl ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑥 ∈ dom 𝑅 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
40 35 39 eqtrd ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → { 𝑓 ∈ ( Base ‘ 𝑃 ) ∣ dom ( 𝑓 ∖ ( 0g ∘ 𝑅 ) ) ∈ Fin } = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )
41 2 40 syl5eq ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ) → 𝐵 = ( Base ‘ ( 𝑆 ⊕m 𝑅 ) ) )