Metamath Proof Explorer


Theorem dsmmelbas

Description: Membership in the finitely supported hull of a structure product in terms of the index set. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmelbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
dsmmelbas.c 𝐶 = ( 𝑆m 𝑅 )
dsmmelbas.b 𝐵 = ( Base ‘ 𝑃 )
dsmmelbas.h 𝐻 = ( Base ‘ 𝐶 )
dsmmelbas.i ( 𝜑𝐼𝑉 )
dsmmelbas.r ( 𝜑𝑅 Fn 𝐼 )
Assertion dsmmelbas ( 𝜑 → ( 𝑋𝐻 ↔ ( 𝑋𝐵 ∧ { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 dsmmelbas.p 𝑃 = ( 𝑆 Xs 𝑅 )
2 dsmmelbas.c 𝐶 = ( 𝑆m 𝑅 )
3 dsmmelbas.b 𝐵 = ( Base ‘ 𝑃 )
4 dsmmelbas.h 𝐻 = ( Base ‘ 𝐶 )
5 dsmmelbas.i ( 𝜑𝐼𝑉 )
6 dsmmelbas.r ( 𝜑𝑅 Fn 𝐼 )
7 2 fveq2i ( Base ‘ 𝐶 ) = ( Base ‘ ( 𝑆m 𝑅 ) )
8 4 7 eqtri 𝐻 = ( Base ‘ ( 𝑆m 𝑅 ) )
9 fnex ( ( 𝑅 Fn 𝐼𝐼𝑉 ) → 𝑅 ∈ V )
10 6 5 9 syl2anc ( 𝜑𝑅 ∈ V )
11 eqid { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } = { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin }
12 11 dsmmbase ( 𝑅 ∈ V → { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆m 𝑅 ) ) )
13 10 12 syl ( 𝜑 → { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } = ( Base ‘ ( 𝑆m 𝑅 ) ) )
14 8 13 eqtr4id ( 𝜑𝐻 = { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } )
15 14 eleq2d ( 𝜑 → ( 𝑋𝐻𝑋 ∈ { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } ) )
16 fveq1 ( 𝑏 = 𝑋 → ( 𝑏𝑎 ) = ( 𝑋𝑎 ) )
17 16 neeq1d ( 𝑏 = 𝑋 → ( ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) ↔ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) ) )
18 17 rabbidv ( 𝑏 = 𝑋 → { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } = { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } )
19 18 eleq1d ( 𝑏 = 𝑋 → ( { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ↔ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) )
20 19 elrab ( 𝑋 ∈ { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } ↔ ( 𝑋 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∧ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) )
21 1 fveq2i ( Base ‘ 𝑃 ) = ( Base ‘ ( 𝑆 Xs 𝑅 ) )
22 3 21 eqtr2i ( Base ‘ ( 𝑆 Xs 𝑅 ) ) = 𝐵
23 22 eleq2i ( 𝑋 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ↔ 𝑋𝐵 )
24 23 a1i ( 𝜑 → ( 𝑋 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ↔ 𝑋𝐵 ) )
25 fndm ( 𝑅 Fn 𝐼 → dom 𝑅 = 𝐼 )
26 rabeq ( dom 𝑅 = 𝐼 → { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } = { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } )
27 6 25 26 3syl ( 𝜑 → { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } = { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } )
28 27 eleq1d ( 𝜑 → ( { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ↔ { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) )
29 24 28 anbi12d ( 𝜑 → ( ( 𝑋 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∧ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) ↔ ( 𝑋𝐵 ∧ { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) ) )
30 20 29 syl5bb ( 𝜑 → ( 𝑋 ∈ { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin } ↔ ( 𝑋𝐵 ∧ { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) ) )
31 15 30 bitrd ( 𝜑 → ( 𝑋𝐻 ↔ ( 𝑋𝐵 ∧ { 𝑎𝐼 ∣ ( 𝑋𝑎 ) ≠ ( 0g ‘ ( 𝑅𝑎 ) ) } ∈ Fin ) ) )