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