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

Proof

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