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		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
10	8 9	syl	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Mnd )
11	10	adantr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 ∈ Mnd )
12		reldmdprd	⊢ Rel dom DProd
13	12	brrelex2i	⊢ ( 𝐺 dom DProd 𝑆 → 𝑆 ∈ V )
14	13	dmexd	⊢ ( 𝐺 dom DProd 𝑆 → dom 𝑆 ∈ V )
15	14	adantr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 ∈ V )
16		simpl	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 dom DProd 𝑆 )
17		eqidd	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 = dom 𝑆 )
18		simpr	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
19	4 16 17 18 1	dprdff	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : dom 𝑆 ⟶ 𝐵 )
20	4 16 17 18 7	dprdfcntz	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
21	4 16 17 18	dprdffsupp	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 finSupp ( 0g ‘ 𝐺 ) )
22	1 3 7 11 15 19 20 21	gsumzcl	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝐺 Σg 𝑓 ) ∈ 𝐵 )
23		eleq1	⊢ ( 𝑥 = ( 𝐺 Σg 𝑓 ) → ( 𝑥 ∈ 𝐵 ↔ ( 𝐺 Σg 𝑓 ) ∈ 𝐵 ) )
24	22 23	syl5ibrcom	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
25	24	rexlimdva	⊢ ( 𝐺 dom DProd 𝑆 → ( ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) → 𝑥 ∈ 𝐵 ) )
26	25	imp	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ dom 𝑆 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } 𝑥 = ( 𝐺 Σg 𝑓 ) ) → 𝑥 ∈ 𝐵 )
27	6 26	sylbi	⊢ ( 𝑥 ∈ ( 𝐺 DProd 𝑆 ) → 𝑥 ∈ 𝐵 )
28	27	ssriv	⊢ ( 𝐺 DProd 𝑆 ) ⊆ 𝐵