Theorem dprdssv

Description: The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypothesis	dprdssv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	dprdssv	⊢ ( 𝐺 DProd 𝑆 ) ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		dprdssv.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		eqid	⊢ dom 𝑆 = dom 𝑆
3		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
4		eqid	⊢ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
5	3 4	eldprd	⊢ ( dom 𝑆 = dom 𝑆 → ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) ) )
6	2 5	ax-mp	⊢ ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) )
7		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
8		dprdgrp	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
9	8	grpmndd	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Mnd )
10	9	adantr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 ∈ Mnd )
11		reldmdprd	⊢ Rel dom DProd
12	11	brrelex2i	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
13	12	dmexd	⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
14	13	adantr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 ∈ V )
15		simpl	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 dom DProd 𝑆 )
16		eqidd	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 = dom 𝑆 )
17		simpr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
18	4 15 16 17 1	dprdff	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : dom 𝑆 ⟶ 𝐵 )
19	4 15 16 17 7	dprdfcntz	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
20	4 15 16 17	dprdffsupp	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 finSupp ( 0g ‘ 𝐺 ) )
21	1 3 7 10 14 18 19 20	gsumzcl	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝐺 Σg 𝑓 ) ∈ 𝐵 )
22		eleq1	⊢ ( 𝑥 = ( 𝐺 Σg 𝑓 ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐺 Σg 𝑓 ) ∈ 𝐵 ) )
23	21 22	syl5ibrcom	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
24	23	rexlimdva	⊢ ( 𝐺 dom DProd 𝑆 → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
25	24	imp	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) → 𝑥 ∈ 𝐵 )
26	6 25	sylbi	⊢ ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) → 𝑥 ∈ 𝐵 )
27	26	ssriv	⊢ ( 𝐺 DProd 𝑆 ) ⊆ 𝐵