This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmdprd

Description: The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016) (Proof shortened by AV, 11-Jul-2019)

Ref Expression
Hypotheses dmdprd.z 
|- Z = ( Cntz ` G )
dmdprd.0 
|- .0. = ( 0g ` G )
dmdprd.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion dmdprd 
|- ( ( I e. V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )

Proof

Step Hyp Ref Expression
1 dmdprd.z 
 |-  Z = ( Cntz ` G )
2 dmdprd.0 
 |-  .0. = ( 0g ` G )
3 dmdprd.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
4 elex 
 |-  ( S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } -> S e. _V )
5 4 a1i 
 |-  ( ( I e. V /\ dom S = I ) -> ( S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } -> S e. _V ) )
6 fex 
 |-  ( ( S : I --> ( SubGrp ` G ) /\ I e. V ) -> S e. _V )
7 6 expcom 
 |-  ( I e. V -> ( S : I --> ( SubGrp ` G ) -> S e. _V ) )
8 7 adantr 
 |-  ( ( I e. V /\ dom S = I ) -> ( S : I --> ( SubGrp ` G ) -> S e. _V ) )
9 8 adantrd 
 |-  ( ( I e. V /\ dom S = I ) -> ( ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) -> S e. _V ) )
10 df-sbc 
 |-  ( [. S / h ]. ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) <-> S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } )
11 simpr 
 |-  ( ( ( I e. V /\ dom S = I ) /\ S e. _V ) -> S e. _V )
12 simpr 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> h = S )
13 12 dmeqd 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> dom h = dom S )
14 simplr 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> dom S = I )
15 13 14 eqtrd 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> dom h = I )
16 12 15 feq12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( h : dom h --> ( SubGrp ` G ) <-> S : I --> ( SubGrp ` G ) ) )
17 15 difeq1d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( dom h \ { x } ) = ( I \ { x } ) )
18 12 fveq1d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( h ` x ) = ( S ` x ) )
19 12 fveq1d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( h ` y ) = ( S ` y ) )
20 19 fveq2d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( Z ` ( h ` y ) ) = ( Z ` ( S ` y ) ) )
21 18 20 sseq12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( ( h ` x ) C_ ( Z ` ( h ` y ) ) <-> ( S ` x ) C_ ( Z ` ( S ` y ) ) ) )
22 17 21 raleqbidv 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) <-> A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) ) )
23 12 17 imaeq12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( h " ( dom h \ { x } ) ) = ( S " ( I \ { x } ) ) )
24 23 unieqd 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> U. ( h " ( dom h \ { x } ) ) = U. ( S " ( I \ { x } ) ) )
25 24 fveq2d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( K ` U. ( h " ( dom h \ { x } ) ) ) = ( K ` U. ( S " ( I \ { x } ) ) ) )
26 18 25 ineq12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) )
27 26 eqeq1d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } <-> ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) )
28 22 27 anbi12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) <-> ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) )
29 15 28 raleqbidv 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) <-> A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) )
30 16 29 anbi12d 
 |-  ( ( ( I e. V /\ dom S = I ) /\ h = S ) -> ( ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
31 30 adantlr 
 |-  ( ( ( ( I e. V /\ dom S = I ) /\ S e. _V ) /\ h = S ) -> ( ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
32 11 31 sbcied 
 |-  ( ( ( I e. V /\ dom S = I ) /\ S e. _V ) -> ( [. S / h ]. ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
33 10 32 bitr3id 
 |-  ( ( ( I e. V /\ dom S = I ) /\ S e. _V ) -> ( S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
34 33 ex 
 |-  ( ( I e. V /\ dom S = I ) -> ( S e. _V -> ( S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) ) )
35 5 9 34 pm5.21ndd 
 |-  ( ( I e. V /\ dom S = I ) -> ( S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } <-> ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
36 35 anbi2d 
 |-  ( ( I e. V /\ dom S = I ) -> ( ( G e. Grp /\ S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } ) <-> ( G e. Grp /\ ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) ) )
37 df-br 
 |-  ( G dom DProd S <-> <. G , S >. e. dom DProd )
38 fvex 
 |-  ( s ` x ) e. _V
39 38 rgenw 
 |-  A. x e. dom s ( s ` x ) e. _V
40 ixpexg 
 |-  ( A. x e. dom s ( s ` x ) e. _V -> X_ x e. dom s ( s ` x ) e. _V )
41 39 40 ax-mp 
 |-  X_ x e. dom s ( s ` x ) e. _V
42 41 mptrabex 
 |-  ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
43 42 rnex 
 |-  ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
44 43 rgen2w 
 |-  A. g e. Grp A. s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
45 df-dprd 
 |-  DProd = ( g e. Grp , s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } |-> ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
46 45 fmpox 
 |-  ( A. g e. Grp A. s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V <-> DProd : U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ) --> _V )
47 44 46 mpbi 
 |-  DProd : U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ) --> _V
48 47 fdmi 
 |-  dom DProd = U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } )
49 48 eleq2i 
 |-  ( <. G , S >. e. dom DProd <-> <. G , S >. e. U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ) )
50 fveq2 
 |-  ( g = G -> ( SubGrp ` g ) = ( SubGrp ` G ) )
51 50 feq3d 
 |-  ( g = G -> ( h : dom h --> ( SubGrp ` g ) <-> h : dom h --> ( SubGrp ` G ) ) )
52 fveq2 
 |-  ( g = G -> ( Cntz ` g ) = ( Cntz ` G ) )
53 52 1 eqtr4di 
 |-  ( g = G -> ( Cntz ` g ) = Z )
54 53 fveq1d 
 |-  ( g = G -> ( ( Cntz ` g ) ` ( h ` y ) ) = ( Z ` ( h ` y ) ) )
55 54 sseq2d 
 |-  ( g = G -> ( ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) <-> ( h ` x ) C_ ( Z ` ( h ` y ) ) ) )
56 55 ralbidv 
 |-  ( g = G -> ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) <-> A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) ) )
57 50 fveq2d 
 |-  ( g = G -> ( mrCls ` ( SubGrp ` g ) ) = ( mrCls ` ( SubGrp ` G ) ) )
58 57 3 eqtr4di 
 |-  ( g = G -> ( mrCls ` ( SubGrp ` g ) ) = K )
59 58 fveq1d 
 |-  ( g = G -> ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) = ( K ` U. ( h " ( dom h \ { x } ) ) ) )
60 59 ineq2d 
 |-  ( g = G -> ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) )
61 fveq2 
 |-  ( g = G -> ( 0g ` g ) = ( 0g ` G ) )
62 61 2 eqtr4di 
 |-  ( g = G -> ( 0g ` g ) = .0. )
63 62 sneqd 
 |-  ( g = G -> { ( 0g ` g ) } = { .0. } )
64 60 63 eqeq12d 
 |-  ( g = G -> ( ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } <-> ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) )
65 56 64 anbi12d 
 |-  ( g = G -> ( ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) <-> ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) )
66 65 ralbidv 
 |-  ( g = G -> ( A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) <-> A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) )
67 51 66 anbi12d 
 |-  ( g = G -> ( ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) <-> ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) ) )
68 67 abbidv 
 |-  ( g = G -> { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } = { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } )
69 68 opeliunxp2 
 |-  ( <. G , S >. e. U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) } ) ) } ) <-> ( G e. Grp /\ S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } ) )
70 37 49 69 3bitri 
 |-  ( G dom DProd S <-> ( G e. Grp /\ S e. { h | ( h : dom h --> ( SubGrp ` G ) /\ A. x e. dom h ( A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( Z ` ( h ` y ) ) /\ ( ( h ` x ) i^i ( K ` U. ( h " ( dom h \ { x } ) ) ) ) = { .0. } ) ) } ) )
71 3anass 
 |-  ( ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) <-> ( G e. Grp /\ ( S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )
72 36 70 71 3bitr4g 
 |-  ( ( I e. V /\ dom S = I ) -> ( G dom DProd S <-> ( G e. Grp /\ S : I --> ( SubGrp ` G ) /\ A. x e. I ( A. y e. ( I \ { x } ) ( S ` x ) C_ ( Z ` ( S ` y ) ) /\ ( ( S ` x ) i^i ( K ` U. ( S " ( I \ { x } ) ) ) ) = { .0. } ) ) ) )