Metamath Proof Explorer


Theorem subgdmdprd

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

Ref Expression
Hypothesis subgdprd.1 H = G 𝑠 A
Assertion subgdmdprd A SubGrp G H dom DProd S G dom DProd S ran S 𝒫 A

Proof

Step Hyp Ref Expression
1 subgdprd.1 H = G 𝑠 A
2 reldmdprd Rel dom DProd
3 2 brrelex2i H dom DProd S S V
4 3 a1i A SubGrp G H dom DProd S S V
5 2 brrelex2i G dom DProd S S V
6 5 adantr G dom DProd S ran S 𝒫 A S V
7 6 a1i A SubGrp G G dom DProd S ran S 𝒫 A S V
8 ffvelrn S : dom S SubGrp H x dom S S x SubGrp H
9 8 ad2ant2lr A SubGrp G S : dom S SubGrp H x dom S y dom S x S x SubGrp H
10 eqid Base H = Base H
11 10 subgss S x SubGrp H S x Base H
12 9 11 syl A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Base H
13 1 subgbas A SubGrp G A = Base H
14 13 ad2antrr A SubGrp G S : dom S SubGrp H x dom S y dom S x A = Base H
15 12 14 sseqtrrd A SubGrp G S : dom S SubGrp H x dom S y dom S x S x A
16 15 biantrud A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x Cntz G S y S x A
17 simpll A SubGrp G S : dom S SubGrp H x dom S y dom S x A SubGrp G
18 simplr A SubGrp G S : dom S SubGrp H x dom S y dom S x S : dom S SubGrp H
19 eldifi y dom S x y dom S
20 19 ad2antll A SubGrp G S : dom S SubGrp H x dom S y dom S x y dom S
21 18 20 ffvelrnd A SubGrp G S : dom S SubGrp H x dom S y dom S x S y SubGrp H
22 10 subgss S y SubGrp H S y Base H
23 21 22 syl A SubGrp G S : dom S SubGrp H x dom S y dom S x S y Base H
24 23 14 sseqtrrd A SubGrp G S : dom S SubGrp H x dom S y dom S x S y A
25 eqid Cntz G = Cntz G
26 eqid Cntz H = Cntz H
27 1 25 26 resscntz A SubGrp G S y A Cntz H S y = Cntz G S y A
28 17 24 27 syl2anc A SubGrp G S : dom S SubGrp H x dom S y dom S x Cntz H S y = Cntz G S y A
29 28 sseq2d A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x Cntz G S y A
30 ssin S x Cntz G S y S x A S x Cntz G S y A
31 29 30 bitr4di A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x Cntz G S y S x A
32 16 31 bitr4d A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x Cntz H S y
33 32 anassrs A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x Cntz H S y
34 33 ralbidva A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y y dom S x S x Cntz H S y
35 subgrcl A SubGrp G G Grp
36 35 ad2antrr A SubGrp G S : dom S SubGrp H x dom S G Grp
37 eqid Base G = Base G
38 37 subgacs G Grp SubGrp G ACS Base G
39 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
40 36 38 39 3syl A SubGrp G S : dom S SubGrp H x dom S SubGrp G Moore Base G
41 1 subggrp A SubGrp G H Grp
42 41 ad2antrr A SubGrp G S : dom S SubGrp H x dom S H Grp
43 10 subgacs H Grp SubGrp H ACS Base H
44 acsmre SubGrp H ACS Base H SubGrp H Moore Base H
45 42 43 44 3syl A SubGrp G S : dom S SubGrp H x dom S SubGrp H Moore Base H
46 eqid mrCls SubGrp H = mrCls SubGrp H
47 imassrn S dom S x ran S
48 frn S : dom S SubGrp H ran S SubGrp H
49 48 ad2antlr A SubGrp G S : dom S SubGrp H x dom S ran S SubGrp H
50 47 49 sstrid A SubGrp G S : dom S SubGrp H x dom S S dom S x SubGrp H
51 mresspw SubGrp H Moore Base H SubGrp H 𝒫 Base H
52 45 51 syl A SubGrp G S : dom S SubGrp H x dom S SubGrp H 𝒫 Base H
53 50 52 sstrd A SubGrp G S : dom S SubGrp H x dom S S dom S x 𝒫 Base H
54 sspwuni S dom S x 𝒫 Base H S dom S x Base H
55 53 54 sylib A SubGrp G S : dom S SubGrp H x dom S S dom S x Base H
56 45 46 55 mrcssidd A SubGrp G S : dom S SubGrp H x dom S S dom S x mrCls SubGrp H S dom S x
57 46 mrccl SubGrp H Moore Base H S dom S x Base H mrCls SubGrp H S dom S x SubGrp H
58 45 55 57 syl2anc A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp H S dom S x SubGrp H
59 1 subsubg A SubGrp G mrCls SubGrp H S dom S x SubGrp H mrCls SubGrp H S dom S x SubGrp G mrCls SubGrp H S dom S x A
60 59 ad2antrr A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp H S dom S x SubGrp H mrCls SubGrp H S dom S x SubGrp G mrCls SubGrp H S dom S x A
61 58 60 mpbid A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp H S dom S x SubGrp G mrCls SubGrp H S dom S x A
62 61 simpld A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp H S dom S x SubGrp G
63 eqid mrCls SubGrp G = mrCls SubGrp G
64 63 mrcsscl SubGrp G Moore Base G S dom S x mrCls SubGrp H S dom S x mrCls SubGrp H S dom S x SubGrp G mrCls SubGrp G S dom S x mrCls SubGrp H S dom S x
65 40 56 62 64 syl3anc A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x mrCls SubGrp H S dom S x
66 13 ad2antrr A SubGrp G S : dom S SubGrp H x dom S A = Base H
67 55 66 sseqtrrd A SubGrp G S : dom S SubGrp H x dom S S dom S x A
68 37 subgss A SubGrp G A Base G
69 68 ad2antrr A SubGrp G S : dom S SubGrp H x dom S A Base G
70 67 69 sstrd A SubGrp G S : dom S SubGrp H x dom S S dom S x Base G
71 40 63 70 mrcssidd A SubGrp G S : dom S SubGrp H x dom S S dom S x mrCls SubGrp G S dom S x
72 63 mrccl SubGrp G Moore Base G S dom S x Base G mrCls SubGrp G S dom S x SubGrp G
73 40 70 72 syl2anc A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x SubGrp G
74 simpll A SubGrp G S : dom S SubGrp H x dom S A SubGrp G
75 63 mrcsscl SubGrp G Moore Base G S dom S x A A SubGrp G mrCls SubGrp G S dom S x A
76 40 67 74 75 syl3anc A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x A
77 1 subsubg A SubGrp G mrCls SubGrp G S dom S x SubGrp H mrCls SubGrp G S dom S x SubGrp G mrCls SubGrp G S dom S x A
78 77 ad2antrr A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x SubGrp H mrCls SubGrp G S dom S x SubGrp G mrCls SubGrp G S dom S x A
79 73 76 78 mpbir2and A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x SubGrp H
80 46 mrcsscl SubGrp H Moore Base H S dom S x mrCls SubGrp G S dom S x mrCls SubGrp G S dom S x SubGrp H mrCls SubGrp H S dom S x mrCls SubGrp G S dom S x
81 45 71 79 80 syl3anc A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp H S dom S x mrCls SubGrp G S dom S x
82 65 81 eqssd A SubGrp G S : dom S SubGrp H x dom S mrCls SubGrp G S dom S x = mrCls SubGrp H S dom S x
83 82 ineq2d A SubGrp G S : dom S SubGrp H x dom S S x mrCls SubGrp G S dom S x = S x mrCls SubGrp H S dom S x
84 eqid 0 G = 0 G
85 1 84 subg0 A SubGrp G 0 G = 0 H
86 85 ad2antrr A SubGrp G S : dom S SubGrp H x dom S 0 G = 0 H
87 86 sneqd A SubGrp G S : dom S SubGrp H x dom S 0 G = 0 H
88 83 87 eqeq12d A SubGrp G S : dom S SubGrp H x dom S S x mrCls SubGrp G S dom S x = 0 G S x mrCls SubGrp H S dom S x = 0 H
89 34 88 anbi12d A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
90 89 ralbidva A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
91 90 pm5.32da A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
92 1 subsubg A SubGrp G x SubGrp H x SubGrp G x A
93 elin x SubGrp G 𝒫 A x SubGrp G x 𝒫 A
94 velpw x 𝒫 A x A
95 94 anbi2i x SubGrp G x 𝒫 A x SubGrp G x A
96 93 95 bitri x SubGrp G 𝒫 A x SubGrp G x A
97 92 96 bitr4di A SubGrp G x SubGrp H x SubGrp G 𝒫 A
98 97 eqrdv A SubGrp G SubGrp H = SubGrp G 𝒫 A
99 98 sseq2d A SubGrp G ran S SubGrp H ran S SubGrp G 𝒫 A
100 ssin ran S SubGrp G ran S 𝒫 A ran S SubGrp G 𝒫 A
101 99 100 bitr4di A SubGrp G ran S SubGrp H ran S SubGrp G ran S 𝒫 A
102 101 anbi2d A SubGrp G S Fn dom S ran S SubGrp H S Fn dom S ran S SubGrp G ran S 𝒫 A
103 df-f S : dom S SubGrp H S Fn dom S ran S SubGrp H
104 df-f S : dom S SubGrp G S Fn dom S ran S SubGrp G
105 104 anbi1i S : dom S SubGrp G ran S 𝒫 A S Fn dom S ran S SubGrp G ran S 𝒫 A
106 anass S Fn dom S ran S SubGrp G ran S 𝒫 A S Fn dom S ran S SubGrp G ran S 𝒫 A
107 105 106 bitri S : dom S SubGrp G ran S 𝒫 A S Fn dom S ran S SubGrp G ran S 𝒫 A
108 102 103 107 3bitr4g A SubGrp G S : dom S SubGrp H S : dom S SubGrp G ran S 𝒫 A
109 108 anbi1d A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G S : dom S SubGrp G ran S 𝒫 A x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
110 91 109 bitr3d A SubGrp G S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H S : dom S SubGrp G ran S 𝒫 A x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
111 110 adantr A SubGrp G S V S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H S : dom S SubGrp G ran S 𝒫 A x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
112 dmexg S V dom S V
113 112 adantl A SubGrp G S V dom S V
114 eqidd A SubGrp G S V dom S = dom S
115 41 adantr A SubGrp G S V H Grp
116 eqid 0 H = 0 H
117 26 116 46 dmdprd dom S V dom S = dom S H dom DProd S H Grp S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
118 3anass H Grp S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H H Grp S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
119 117 118 bitrdi dom S V dom S = dom S H dom DProd S H Grp S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
120 119 baibd dom S V dom S = dom S H Grp H dom DProd S S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
121 113 114 115 120 syl21anc A SubGrp G S V H dom DProd S S : dom S SubGrp H x dom S y dom S x S x Cntz H S y S x mrCls SubGrp H S dom S x = 0 H
122 35 adantr A SubGrp G S V G Grp
123 25 84 63 dmdprd dom S V dom S = dom S G dom DProd S G Grp S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
124 3anass G Grp S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G G Grp S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
125 123 124 bitrdi dom S V dom S = dom S G dom DProd S G Grp S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
126 125 baibd dom S V dom S = dom S G Grp G dom DProd S S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
127 113 114 122 126 syl21anc A SubGrp G S V G dom DProd S S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
128 127 anbi1d A SubGrp G S V G dom DProd S ran S 𝒫 A S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G ran S 𝒫 A
129 an32 S : dom S SubGrp G x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G ran S 𝒫 A S : dom S SubGrp G ran S 𝒫 A x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
130 128 129 bitrdi A SubGrp G S V G dom DProd S ran S 𝒫 A S : dom S SubGrp G ran S 𝒫 A x dom S y dom S x S x Cntz G S y S x mrCls SubGrp G S dom S x = 0 G
131 111 121 130 3bitr4d A SubGrp G S V H dom DProd S G dom DProd S ran S 𝒫 A
132 131 ex A SubGrp G S V H dom DProd S G dom DProd S ran S 𝒫 A
133 4 7 132 pm5.21ndd A SubGrp G H dom DProd S G dom DProd S ran S 𝒫 A