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