Theorem dprdlub

Description: The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdlub.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dprdlub.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dprdlub.3	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	dprdlub.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
Assertion	dprdlub	⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		dprdlub.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dprdlub.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dprdlub.3	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4		dprdlub.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6		eqid	⊢ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) }
7	5 6	dprdval	⊢ ( ( 𝐺 dom DProd 𝑆 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) )
9		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
10	1	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 dom DProd 𝑆 )
11		dprdgrp	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
12		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
13	10 11 12	3syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐺 ∈ Mnd )
14	1 2	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝐼 ∈ V )
16	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
17		subgsubm	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
18	16 17	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
19	2	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → dom 𝑆 = 𝐼 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } )
21		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22	6 10 19 20 21	dprdff	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
23	22	ffnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 Fn 𝐼 )
24	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑘 ) ⊆ 𝑇 )
25	6 10 19 20	dprdfcl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝑆 ‘ 𝑘 ) )
26	24 25	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 )
27	26	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ∀ 𝑘 ∈ 𝐼 ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 )
28		ffnfv	⊢ ( 𝑓 : 𝐼 ⟶ 𝑇 ↔ ( 𝑓 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑓 ‘ 𝑘 ) ∈ 𝑇 ) )
29	23 27 28	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 : 𝐼 ⟶ 𝑇 )
30	6 10 19 20 9	dprdfcntz	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ran 𝑓 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝑓 ) )
31	6 10 19 20	dprdffsupp	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → 𝑓 finSupp ( 0g ‘ 𝐺 ) )
32	5 9 13 15 18 29 30 31	gsumzsubmcl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ) → ( 𝐺 Σg 𝑓 ) ∈ 𝑇 )
33	32	fmpttd	⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) : { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ⟶ 𝑇 )
34	33	frnd	⊢ ( 𝜑 → ran ( 𝑓 ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp ( 0g ‘ 𝐺 ) } ↦ ( 𝐺 Σg 𝑓 ) ) ⊆ 𝑇 )
35	8 34	eqsstrd	⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ 𝑇 )