Metamath Proof Explorer


Theorem eldprd

Description: A class A is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Hypotheses dprdval.0
|- .0. = ( 0g ` G )
dprdval.w
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
Assertion eldprd
|- ( dom S = I -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsum f ) ) ) )

Proof

Step Hyp Ref Expression
1 dprdval.0
 |-  .0. = ( 0g ` G )
2 dprdval.w
 |-  W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3 elfvdm
 |-  ( A e. ( DProd ` <. G , S >. ) -> <. G , S >. e. dom DProd )
4 df-ov
 |-  ( G DProd S ) = ( DProd ` <. G , S >. )
5 3 4 eleq2s
 |-  ( A e. ( G DProd S ) -> <. G , S >. e. dom DProd )
6 df-br
 |-  ( G dom DProd S <-> <. G , S >. e. dom DProd )
7 5 6 sylibr
 |-  ( A e. ( G DProd S ) -> G dom DProd S )
8 7 pm4.71ri
 |-  ( A e. ( G DProd S ) <-> ( G dom DProd S /\ A e. ( G DProd S ) ) )
9 1 2 dprdval
 |-  ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) )
10 9 eleq2d
 |-  ( ( G dom DProd S /\ dom S = I ) -> ( A e. ( G DProd S ) <-> A e. ran ( f e. W |-> ( G gsum f ) ) ) )
11 eqid
 |-  ( f e. W |-> ( G gsum f ) ) = ( f e. W |-> ( G gsum f ) )
12 ovex
 |-  ( G gsum f ) e. _V
13 11 12 elrnmpti
 |-  ( A e. ran ( f e. W |-> ( G gsum f ) ) <-> E. f e. W A = ( G gsum f ) )
14 10 13 bitrdi
 |-  ( ( G dom DProd S /\ dom S = I ) -> ( A e. ( G DProd S ) <-> E. f e. W A = ( G gsum f ) ) )
15 14 ancoms
 |-  ( ( dom S = I /\ G dom DProd S ) -> ( A e. ( G DProd S ) <-> E. f e. W A = ( G gsum f ) ) )
16 15 pm5.32da
 |-  ( dom S = I -> ( ( G dom DProd S /\ A e. ( G DProd S ) ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsum f ) ) ) )
17 8 16 syl5bb
 |-  ( dom S = I -> ( A e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. W A = ( G gsum f ) ) ) )