Metamath Proof Explorer

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 ⊢ φ → G dom ⁡ DProd S
dprdlub.2 ⊢ φ → dom ⁡ S = I
dprdlub.3 ⊢ φ → T ∈ SubGrp ⁡ G
dprdlub.4 ⊢ φ ∧ k ∈ I → S ⁡ k ⊆ T
Assertion dprdlub ⊢ φ → G DProd S ⊆ T

Proof

Step Hyp Ref Expression
1 dprdlub.1 ⊢ φ → G dom ⁡ DProd S
2 dprdlub.2 ⊢ φ → dom ⁡ S = I
3 dprdlub.3 ⊢ φ → T ∈ SubGrp ⁡ G
4 dprdlub.4 ⊢ φ ∧ k ∈ I → S ⁡ k ⊆ T
5 eqid ⊢ 0 G = 0 G
6 eqid ⊢ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h
7 5 6 dprdval ⊢ G dom ⁡ DProd S ∧ dom ⁡ S = I → G DProd S = ran ⁡ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ⟼ ∑ G f
8 1 2 7 syl2anc ⊢ φ → G DProd S = ran ⁡ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ⟼ ∑ G f
9 eqid ⊢ Cntz ⁡ G = Cntz ⁡ G
10 1 adantr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → G dom ⁡ DProd S
11 dprdgrp ⊢ G dom ⁡ DProd S → G ∈ Grp
12 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
13 10 11 12 3syl ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → G ∈ Mnd
14 1 2 dprddomcld ⊢ φ → I ∈ V
15 14 adantr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → I ∈ V
16 3 adantr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → T ∈ SubGrp ⁡ G
17 subgsubm ⊢ T ∈ SubGrp ⁡ G → T ∈ SubMnd ⁡ G
18 16 17 syl ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → T ∈ SubMnd ⁡ G
19 2 adantr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → dom ⁡ S = I
20 simpr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h
21 eqid ⊢ Base G = Base G
22 6 10 19 20 21 dprdff ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → f : I ⟶ Base G
23 22 ffnd ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → f Fn I
24 4 adantlr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ∧ k ∈ I → S ⁡ k ⊆ T
25 6 10 19 20 dprdfcl ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ∧ k ∈ I → f ⁡ k ∈ S ⁡ k
26 24 25 sseldd ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ∧ k ∈ I → f ⁡ k ∈ T
27 26 ralrimiva ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → ∀ k ∈ I f ⁡ k ∈ T
28 ffnfv ⊢ f : I ⟶ T ↔ f Fn I ∧ ∀ k ∈ I f ⁡ k ∈ T
29 23 27 28 sylanbrc ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → f : I ⟶ T
30 6 10 19 20 9 dprdfcntz ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → ran ⁡ f ⊆ Cntz ⁡ G ⁡ ran ⁡ f
31 6 10 19 20 dprdffsupp ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → finSupp 0 G⁡ f
32 5 9 13 15 18 29 30 31 gsumzsubmcl ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h → ∑ G f ∈ T
33 32 fmpttd ⊢ φ → f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ⟼ ∑ G f : h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ⟶ T
34 33 frnd ⊢ φ → ran ⁡ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 G⁡ h ⟼ ∑ G f ⊆ T
35 8 34 eqsstrd ⊢ φ → G DProd S ⊆ T