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

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 bitrid ⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑏 ∈ ( Base ‘ ( 𝑆 Xs 𝑅 ) ) ∣ { 𝑎 ∈ dom 𝑅 ∣ ( 𝑏 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin } ↔ ( 𝑋 ∈ 𝐵 ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝑋 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )
31 15 30 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐻 ↔ ( 𝑋 ∈ 𝐵 ∧ { 𝑎 ∈ 𝐼 ∣ ( 𝑋 ‘ 𝑎 ) ≠ ( 0g ‘ ( 𝑅 ‘ 𝑎 ) ) } ∈ Fin ) ) )