Metamath Proof Explorer


Theorem subgdprd

Description: A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses subgdprd.1 H = G 𝑠 A
subgdprd.2 φ A SubGrp G
subgdprd.3 φ G dom DProd S
subgdprd.4 φ ran S 𝒫 A
Assertion subgdprd φ H DProd S = G DProd S

Proof

Step Hyp Ref Expression
1 subgdprd.1 H = G 𝑠 A
2 subgdprd.2 φ A SubGrp G
3 subgdprd.3 φ G dom DProd S
4 subgdprd.4 φ ran S 𝒫 A
5 1 subggrp A SubGrp G H Grp
6 2 5 syl φ H Grp
7 eqid Base H = Base H
8 7 subgacs H Grp SubGrp H ACS Base H
9 acsmre SubGrp H ACS Base H SubGrp H Moore Base H
10 6 8 9 3syl φ SubGrp H Moore Base H
11 subgrcl A SubGrp G G Grp
12 2 11 syl φ G Grp
13 eqid Base G = Base G
14 13 subgacs G Grp SubGrp G ACS Base G
15 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
16 12 14 15 3syl φ SubGrp G Moore Base G
17 eqid mrCls SubGrp G = mrCls SubGrp G
18 dprdf G dom DProd S S : dom S SubGrp G
19 frn S : dom S SubGrp G ran S SubGrp G
20 3 18 19 3syl φ ran S SubGrp G
21 mresspw SubGrp G Moore Base G SubGrp G 𝒫 Base G
22 16 21 syl φ SubGrp G 𝒫 Base G
23 20 22 sstrd φ ran S 𝒫 Base G
24 sspwuni ran S 𝒫 Base G ran S Base G
25 23 24 sylib φ ran S Base G
26 16 17 25 mrcssidd φ ran S mrCls SubGrp G ran S
27 17 mrccl SubGrp G Moore Base G ran S Base G mrCls SubGrp G ran S SubGrp G
28 16 25 27 syl2anc φ mrCls SubGrp G ran S SubGrp G
29 sspwuni ran S 𝒫 A ran S A
30 4 29 sylib φ ran S A
31 17 mrcsscl SubGrp G Moore Base G ran S A A SubGrp G mrCls SubGrp G ran S A
32 16 30 2 31 syl3anc φ mrCls SubGrp G ran S A
33 1 subsubg A SubGrp G mrCls SubGrp G ran S SubGrp H mrCls SubGrp G ran S SubGrp G mrCls SubGrp G ran S A
34 2 33 syl φ mrCls SubGrp G ran S SubGrp H mrCls SubGrp G ran S SubGrp G mrCls SubGrp G ran S A
35 28 32 34 mpbir2and φ mrCls SubGrp G ran S SubGrp H
36 eqid mrCls SubGrp H = mrCls SubGrp H
37 36 mrcsscl SubGrp H Moore Base H ran S mrCls SubGrp G ran S mrCls SubGrp G ran S SubGrp H mrCls SubGrp H ran S mrCls SubGrp G ran S
38 10 26 35 37 syl3anc φ mrCls SubGrp H ran S mrCls SubGrp G ran S
39 1 subgdmdprd A SubGrp G H dom DProd S G dom DProd S ran S 𝒫 A
40 2 39 syl φ H dom DProd S G dom DProd S ran S 𝒫 A
41 3 4 40 mpbir2and φ H dom DProd S
42 eqidd φ dom S = dom S
43 41 42 dprdf2 φ S : dom S SubGrp H
44 43 frnd φ ran S SubGrp H
45 mresspw SubGrp H Moore Base H SubGrp H 𝒫 Base H
46 10 45 syl φ SubGrp H 𝒫 Base H
47 44 46 sstrd φ ran S 𝒫 Base H
48 sspwuni ran S 𝒫 Base H ran S Base H
49 47 48 sylib φ ran S Base H
50 10 36 49 mrcssidd φ ran S mrCls SubGrp H ran S
51 36 mrccl SubGrp H Moore Base H ran S Base H mrCls SubGrp H ran S SubGrp H
52 10 49 51 syl2anc φ mrCls SubGrp H ran S SubGrp H
53 1 subsubg A SubGrp G mrCls SubGrp H ran S SubGrp H mrCls SubGrp H ran S SubGrp G mrCls SubGrp H ran S A
54 2 53 syl φ mrCls SubGrp H ran S SubGrp H mrCls SubGrp H ran S SubGrp G mrCls SubGrp H ran S A
55 52 54 mpbid φ mrCls SubGrp H ran S SubGrp G mrCls SubGrp H ran S A
56 55 simpld φ mrCls SubGrp H ran S SubGrp G
57 17 mrcsscl SubGrp G Moore Base G ran S mrCls SubGrp H ran S mrCls SubGrp H ran S SubGrp G mrCls SubGrp G ran S mrCls SubGrp H ran S
58 16 50 56 57 syl3anc φ mrCls SubGrp G ran S mrCls SubGrp H ran S
59 38 58 eqssd φ mrCls SubGrp H ran S = mrCls SubGrp G ran S
60 36 dprdspan H dom DProd S H DProd S = mrCls SubGrp H ran S
61 41 60 syl φ H DProd S = mrCls SubGrp H ran S
62 17 dprdspan G dom DProd S G DProd S = mrCls SubGrp G ran S
63 3 62 syl φ G DProd S = mrCls SubGrp G ran S
64 59 61 63 3eqtr4d φ H DProd S = G DProd S