Metamath Proof Explorer


Theorem dprdsubg

Description: The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdsubg GdomDProdSGDProdSSubGrpG

Proof

Step Hyp Ref Expression
1 eqid BaseG=BaseG
2 1 dprdssv GDProdSBaseG
3 2 a1i GdomDProdSGDProdSBaseG
4 eqid 0G=0G
5 eqid hidomSSi|finSupp0Gh=hidomSSi|finSupp0Gh
6 id GdomDProdSGdomDProdS
7 eqidd GdomDProdSdomS=domS
8 fvex 0GV
9 fnconstg 0GVdomS×0GFndomS
10 8 9 mp1i GdomDProdSdomS×0GFndomS
11 8 fvconst2 kdomSdomS×0Gk=0G
12 11 adantl GdomDProdSkdomSdomS×0Gk=0G
13 dprdf GdomDProdSS:domSSubGrpG
14 13 ffvelcdmda GdomDProdSkdomSSkSubGrpG
15 4 subg0cl SkSubGrpG0GSk
16 14 15 syl GdomDProdSkdomS0GSk
17 12 16 eqeltrd GdomDProdSkdomSdomS×0GkSk
18 17 ralrimiva GdomDProdSkdomSdomS×0GkSk
19 df-nel domSV¬domSV
20 dprddomprc domSV¬GdomDProdS
21 19 20 sylbir ¬domSV¬GdomDProdS
22 21 con4i GdomDProdSdomSV
23 8 a1i GdomDProdS0GV
24 22 23 fczfsuppd GdomDProdSfinSupp0GdomS×0G
25 5 6 7 dprdw GdomDProdSdomS×0GhidomSSi|finSupp0GhdomS×0GFndomSkdomSdomS×0GkSkfinSupp0GdomS×0G
26 10 18 24 25 mpbir3and GdomDProdSdomS×0GhidomSSi|finSupp0Gh
27 4 5 6 7 26 eldprdi GdomDProdSGdomS×0GGDProdS
28 27 ne0d GdomDProdSGDProdS
29 eqid domS=domS
30 4 5 eldprd domS=domSxGDProdSGdomDProdSfhidomSSi|finSupp0Ghx=Gf
31 30 baibd domS=domSGdomDProdSxGDProdSfhidomSSi|finSupp0Ghx=Gf
32 4 5 eldprd domS=domSyGDProdSGdomDProdSghidomSSi|finSupp0Ghy=Gg
33 32 baibd domS=domSGdomDProdSyGDProdSghidomSSi|finSupp0Ghy=Gg
34 31 33 anbi12d domS=domSGdomDProdSxGDProdSyGDProdSfhidomSSi|finSupp0Ghx=GfghidomSSi|finSupp0Ghy=Gg
35 29 34 mpan GdomDProdSxGDProdSyGDProdSfhidomSSi|finSupp0Ghx=GfghidomSSi|finSupp0Ghy=Gg
36 reeanv fhidomSSi|finSupp0GhghidomSSi|finSupp0Ghx=Gfy=GgfhidomSSi|finSupp0Ghx=GfghidomSSi|finSupp0Ghy=Gg
37 simpl GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhGdomDProdS
38 eqidd GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhdomS=domS
39 simprl GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhfhidomSSi|finSupp0Gh
40 simprr GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhghidomSSi|finSupp0Gh
41 eqid -G=-G
42 4 5 37 38 39 40 41 dprdfsub GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0Ghf-GfghidomSSi|finSupp0GhGf-Gfg=Gf-GGg
43 42 simprd GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhGf-Gfg=Gf-GGg
44 42 simpld GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0Ghf-GfghidomSSi|finSupp0Gh
45 4 5 37 38 44 eldprdi GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhGf-GfgGDProdS
46 43 45 eqeltrrd GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0GhGf-GGgGDProdS
47 oveq12 x=Gfy=Ggx-Gy=Gf-GGg
48 47 eleq1d x=Gfy=Ggx-GyGDProdSGf-GGgGDProdS
49 46 48 syl5ibrcom GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0Ghx=Gfy=Ggx-GyGDProdS
50 49 rexlimdvva GdomDProdSfhidomSSi|finSupp0GhghidomSSi|finSupp0Ghx=Gfy=Ggx-GyGDProdS
51 36 50 biimtrrid GdomDProdSfhidomSSi|finSupp0Ghx=GfghidomSSi|finSupp0Ghy=Ggx-GyGDProdS
52 35 51 sylbid GdomDProdSxGDProdSyGDProdSx-GyGDProdS
53 52 ralrimivv GdomDProdSxGDProdSyGDProdSx-GyGDProdS
54 dprdgrp GdomDProdSGGrp
55 1 41 issubg4 GGrpGDProdSSubGrpGGDProdSBaseGGDProdSxGDProdSyGDProdSx-GyGDProdS
56 54 55 syl GdomDProdSGDProdSSubGrpGGDProdSBaseGGDProdSxGDProdSyGDProdSx-GyGDProdS
57 3 28 53 56 mpbir3and GdomDProdSGDProdSSubGrpG