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 
|- ( ph -> G dom DProd S )
dprdlub.2 
|- ( ph -> dom S = I )
dprdlub.3 
|- ( ph -> T e. ( SubGrp ` G ) )
dprdlub.4 
|- ( ( ph /\ k e. I ) -> ( S ` k ) C_ T )
Assertion dprdlub 
|- ( ph -> ( G DProd S ) C_ T )

Proof

Step Hyp Ref Expression
1 dprdlub.1 
 |-  ( ph -> G dom DProd S )
2 dprdlub.2 
 |-  ( ph -> dom S = I )
3 dprdlub.3 
 |-  ( ph -> T e. ( SubGrp ` G ) )
4 dprdlub.4 
 |-  ( ( ph /\ k e. I ) -> ( S ` k ) C_ T )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 eqid 
 |-  { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } = { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) }
7 5 6 dprdval 
 |-  ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } |-> ( G gsum f ) ) )
8 1 2 7 syl2anc 
 |-  ( ph -> ( G DProd S ) = ran ( f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } |-> ( G gsum f ) ) )
9 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
10 1 adantr 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> G dom DProd S )
11 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
12 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
13 10 11 12 3syl 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> G e. Mnd )
14 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
15 14 adantr 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> I e. _V )
16 3 adantr 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> T e. ( SubGrp ` G ) )
17 subgsubm 
 |-  ( T e. ( SubGrp ` G ) -> T e. ( SubMnd ` G ) )
18 16 17 syl 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> T e. ( SubMnd ` G ) )
19 2 adantr 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> dom S = I )
20 simpr 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } )
21 eqid 
 |-  ( Base ` G ) = ( Base ` G )
22 6 10 19 20 21 dprdff 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f : I --> ( Base ` G ) )
23 22 ffnd 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f Fn I )
24 4 adantlr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) /\ k e. I ) -> ( S ` k ) C_ T )
25 6 10 19 20 dprdfcl 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) /\ k e. I ) -> ( f ` k ) e. ( S ` k ) )
26 24 25 sseldd 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) /\ k e. I ) -> ( f ` k ) e. T )
27 26 ralrimiva 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> A. k e. I ( f ` k ) e. T )
28 ffnfv 
 |-  ( f : I --> T <-> ( f Fn I /\ A. k e. I ( f ` k ) e. T ) )
29 23 27 28 sylanbrc 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f : I --> T )
30 6 10 19 20 9 dprdfcntz 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> ran f C_ ( ( Cntz ` G ) ` ran f ) )
31 6 10 19 20 dprdffsupp 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> f finSupp ( 0g ` G ) )
32 5 9 13 15 18 29 30 31 gsumzsubmcl 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } ) -> ( G gsum f ) e. T )
33 32 fmpttd 
 |-  ( ph -> ( f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } |-> ( G gsum f ) ) : { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } --> T )
34 33 frnd 
 |-  ( ph -> ran ( f e. { h e. X_ i e. I ( S ` i ) | h finSupp ( 0g ` G ) } |-> ( G gsum f ) ) C_ T )
35 8 34 eqsstrd 
 |-  ( ph -> ( G DProd S ) C_ T )