MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprdss Structured version   Visualization version   GIF version

Theorem dprdss 18695
Description: Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016.)
Hypotheses
Ref Expression
dprdss.1 (𝜑𝐺dom DProd 𝑇)
dprdss.2 (𝜑 → dom 𝑇 = 𝐼)
dprdss.3 (𝜑𝑆:𝐼⟶(SubGrp‘𝐺))
dprdss.4 ((𝜑𝑘𝐼) → (𝑆𝑘) ⊆ (𝑇𝑘))
Assertion
Ref Expression
dprdss (𝜑 → (𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇)))
Distinct variable groups:   𝑘,𝐺   𝜑,𝑘   𝑆,𝑘   𝑇,𝑘   𝑘,𝐼

Proof of Theorem dprdss
Dummy variables 𝑓 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2765 . . 3 (Cntz‘𝐺) = (Cntz‘𝐺)
2 eqid 2765 . . 3 (0g𝐺) = (0g𝐺)
3 eqid 2765 . . 3 (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4 dprdss.1 . . . 4 (𝜑𝐺dom DProd 𝑇)
5 dprdgrp 18671 . . . 4 (𝐺dom DProd 𝑇𝐺 ∈ Grp)
64, 5syl 17 . . 3 (𝜑𝐺 ∈ Grp)
7 dprdss.2 . . . 4 (𝜑 → dom 𝑇 = 𝐼)
84, 7dprddomcld 18667 . . 3 (𝜑𝐼 ∈ V)
9 dprdss.3 . . 3 (𝜑𝑆:𝐼⟶(SubGrp‘𝐺))
10 dprdss.4 . . . . . . 7 ((𝜑𝑘𝐼) → (𝑆𝑘) ⊆ (𝑇𝑘))
1110ralrimiva 3113 . . . . . 6 (𝜑 → ∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘))
12 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑥 → (𝑆𝑘) = (𝑆𝑥))
13 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑥 → (𝑇𝑘) = (𝑇𝑥))
1412, 13sseq12d 3794 . . . . . . 7 (𝑘 = 𝑥 → ((𝑆𝑘) ⊆ (𝑇𝑘) ↔ (𝑆𝑥) ⊆ (𝑇𝑥)))
1514rspcv 3457 . . . . . 6 (𝑥𝐼 → (∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘) → (𝑆𝑥) ⊆ (𝑇𝑥)))
1611, 15mpan9 502 . . . . 5 ((𝜑𝑥𝐼) → (𝑆𝑥) ⊆ (𝑇𝑥))
17163ad2antr1 1239 . . . 4 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑆𝑥) ⊆ (𝑇𝑥))
184adantr 472 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → 𝐺dom DProd 𝑇)
197adantr 472 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → dom 𝑇 = 𝐼)
20 simpr1 1248 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → 𝑥𝐼)
21 simpr2 1250 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → 𝑦𝐼)
22 simpr3 1252 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → 𝑥𝑦)
2318, 19, 20, 21, 22, 1dprdcntz 18674 . . . . 5 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑇𝑥) ⊆ ((Cntz‘𝐺)‘(𝑇𝑦)))
244, 7dprdf2 18673 . . . . . . . . 9 (𝜑𝑇:𝐼⟶(SubGrp‘𝐺))
2524adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → 𝑇:𝐼⟶(SubGrp‘𝐺))
2625, 21ffvelrnd 6550 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑇𝑦) ∈ (SubGrp‘𝐺))
27 eqid 2765 . . . . . . . 8 (Base‘𝐺) = (Base‘𝐺)
2827subgss 17859 . . . . . . 7 ((𝑇𝑦) ∈ (SubGrp‘𝐺) → (𝑇𝑦) ⊆ (Base‘𝐺))
2926, 28syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑇𝑦) ⊆ (Base‘𝐺))
30 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑦 → (𝑆𝑘) = (𝑆𝑦))
31 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑦 → (𝑇𝑘) = (𝑇𝑦))
3230, 31sseq12d 3794 . . . . . . 7 (𝑘 = 𝑦 → ((𝑆𝑘) ⊆ (𝑇𝑘) ↔ (𝑆𝑦) ⊆ (𝑇𝑦)))
3311adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → ∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘))
3432, 33, 21rspcdva 3467 . . . . . 6 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑆𝑦) ⊆ (𝑇𝑦))
3527, 1cntz2ss 18028 . . . . . 6 (((𝑇𝑦) ⊆ (Base‘𝐺) ∧ (𝑆𝑦) ⊆ (𝑇𝑦)) → ((Cntz‘𝐺)‘(𝑇𝑦)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
3629, 34, 35syl2anc 579 . . . . 5 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → ((Cntz‘𝐺)‘(𝑇𝑦)) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
3723, 36sstrd 3771 . . . 4 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑇𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
3817, 37sstrd 3771 . . 3 ((𝜑 ∧ (𝑥𝐼𝑦𝐼𝑥𝑦)) → (𝑆𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆𝑦)))
396adantr 472 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐺 ∈ Grp)
4027subgacs 17893 . . . . . . 7 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
41 acsmre 16578 . . . . . . 7 ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
4239, 40, 413syl 18 . . . . . 6 ((𝜑𝑥𝐼) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
43 difss 3899 . . . . . . . . 9 (𝐼 ∖ {𝑥}) ⊆ 𝐼
4411adantr 472 . . . . . . . . 9 ((𝜑𝑥𝐼) → ∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘))
45 ssralv 3826 . . . . . . . . 9 ((𝐼 ∖ {𝑥}) ⊆ 𝐼 → (∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘) → ∀𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) ⊆ (𝑇𝑘)))
4643, 44, 45mpsyl 68 . . . . . . . 8 ((𝜑𝑥𝐼) → ∀𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) ⊆ (𝑇𝑘))
47 ss2iun 4692 . . . . . . . 8 (∀𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) ⊆ (𝑇𝑘) → 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) ⊆ 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇𝑘))
4846, 47syl 17 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) ⊆ 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇𝑘))
499adantr 472 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑆:𝐼⟶(SubGrp‘𝐺))
50 ffun 6226 . . . . . . . 8 (𝑆:𝐼⟶(SubGrp‘𝐺) → Fun 𝑆)
51 funiunfv 6698 . . . . . . . 8 (Fun 𝑆 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) = (𝑆 “ (𝐼 ∖ {𝑥})))
5249, 50, 513syl 18 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑆𝑘) = (𝑆 “ (𝐼 ∖ {𝑥})))
5324adantr 472 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑇:𝐼⟶(SubGrp‘𝐺))
54 ffun 6226 . . . . . . . 8 (𝑇:𝐼⟶(SubGrp‘𝐺) → Fun 𝑇)
55 funiunfv 6698 . . . . . . . 8 (Fun 𝑇 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇𝑘) = (𝑇 “ (𝐼 ∖ {𝑥})))
5653, 54, 553syl 18 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑘 ∈ (𝐼 ∖ {𝑥})(𝑇𝑘) = (𝑇 “ (𝐼 ∖ {𝑥})))
5748, 52, 563sstr3d 3807 . . . . . 6 ((𝜑𝑥𝐼) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (𝑇 “ (𝐼 ∖ {𝑥})))
58 imassrn 5659 . . . . . . . 8 (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑇
5953frnd 6230 . . . . . . . . 9 ((𝜑𝑥𝐼) → ran 𝑇 ⊆ (SubGrp‘𝐺))
60 mresspw 16518 . . . . . . . . . 10 ((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
6142, 60syl 17 . . . . . . . . 9 ((𝜑𝑥𝐼) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺))
6259, 61sstrd 3771 . . . . . . . 8 ((𝜑𝑥𝐼) → ran 𝑇 ⊆ 𝒫 (Base‘𝐺))
6358, 62syl5ss 3772 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺))
64 sspwuni 4768 . . . . . . 7 ((𝑇 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺))
6563, 64sylib 209 . . . . . 6 ((𝜑𝑥𝐼) → (𝑇 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺))
6642, 3, 57, 65mrcssd 16550 . . . . 5 ((𝜑𝑥𝐼) → ((mrCls‘(SubGrp‘𝐺))‘ (𝑆 “ (𝐼 ∖ {𝑥}))) ⊆ ((mrCls‘(SubGrp‘𝐺))‘ (𝑇 “ (𝐼 ∖ {𝑥}))))
67 ss2in 4000 . . . . 5 (((𝑆𝑥) ⊆ (𝑇𝑥) ∧ ((mrCls‘(SubGrp‘𝐺))‘ (𝑆 “ (𝐼 ∖ {𝑥}))) ⊆ ((mrCls‘(SubGrp‘𝐺))‘ (𝑇 “ (𝐼 ∖ {𝑥})))) → ((𝑆𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ ((𝑇𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑇 “ (𝐼 ∖ {𝑥})))))
6816, 66, 67syl2anc 579 . . . 4 ((𝜑𝑥𝐼) → ((𝑆𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ ((𝑇𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑇 “ (𝐼 ∖ {𝑥})))))
694adantr 472 . . . . 5 ((𝜑𝑥𝐼) → 𝐺dom DProd 𝑇)
707adantr 472 . . . . 5 ((𝜑𝑥𝐼) → dom 𝑇 = 𝐼)
71 simpr 477 . . . . 5 ((𝜑𝑥𝐼) → 𝑥𝐼)
7269, 70, 71, 2, 3dprddisj 18675 . . . 4 ((𝜑𝑥𝐼) → ((𝑇𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑇 “ (𝐼 ∖ {𝑥})))) = {(0g𝐺)})
7368, 72sseqtrd 3801 . . 3 ((𝜑𝑥𝐼) → ((𝑆𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ {(0g𝐺)})
741, 2, 3, 6, 8, 9, 38, 73dmdprdd 18665 . 2 (𝜑𝐺dom DProd 𝑆)
754a1d 25 . . . . 5 (𝜑 → (𝐺dom DProd 𝑆𝐺dom DProd 𝑇))
76 ss2ixp 8126 . . . . . . 7 (∀𝑘𝐼 (𝑆𝑘) ⊆ (𝑇𝑘) → X𝑘𝐼 (𝑆𝑘) ⊆ X𝑘𝐼 (𝑇𝑘))
7711, 76syl 17 . . . . . 6 (𝜑X𝑘𝐼 (𝑆𝑘) ⊆ X𝑘𝐼 (𝑇𝑘))
78 rabss2 3845 . . . . . 6 (X𝑘𝐼 (𝑆𝑘) ⊆ X𝑘𝐼 (𝑇𝑘) → {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)} ⊆ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)})
79 ssrexv 3827 . . . . . 6 ({X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)} ⊆ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)} → (∃𝑓 ∈ {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓) → ∃𝑓 ∈ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓)))
8077, 78, 793syl 18 . . . . 5 (𝜑 → (∃𝑓 ∈ {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓) → ∃𝑓 ∈ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓)))
8175, 80anim12d 602 . . . 4 (𝜑 → ((𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓)) → (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓))))
82 fdm 6231 . . . . 5 (𝑆:𝐼⟶(SubGrp‘𝐺) → dom 𝑆 = 𝐼)
83 eqid 2765 . . . . . 6 {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)} = {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}
842, 83eldprd 18670 . . . . 5 (dom 𝑆 = 𝐼 → (𝑎 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓))))
859, 82, 843syl 18 . . . 4 (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑆𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓))))
86 eqid 2765 . . . . . 6 {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)} = {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}
872, 86eldprd 18670 . . . . 5 (dom 𝑇 = 𝐼 → (𝑎 ∈ (𝐺 DProd 𝑇) ↔ (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓))))
887, 87syl 17 . . . 4 (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑇) ↔ (𝐺dom DProd 𝑇 ∧ ∃𝑓 ∈ {X𝑘𝐼 (𝑇𝑘) ∣ finSupp (0g𝐺)}𝑎 = (𝐺 Σg 𝑓))))
8981, 85, 883imtr4d 285 . . 3 (𝜑 → (𝑎 ∈ (𝐺 DProd 𝑆) → 𝑎 ∈ (𝐺 DProd 𝑇)))
9089ssrdv 3767 . 2 (𝜑 → (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇))
9174, 90jca 507 1 (𝜑 → (𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cin 3731  wss 3732  𝒫 cpw 4315  {csn 4334   cuni 4594   ciun 4676   class class class wbr 4809  dom cdm 5277  ran crn 5278  cima 5280  Fun wfun 6062  wf 6064  cfv 6068  (class class class)co 6842  Xcixp 8113   finSupp cfsupp 8482  Basecbs 16130  0gc0g 16366   Σg cgsu 16367  Moorecmre 16508  mrClscmrc 16509  ACScacs 16511  Grpcgrp 17689  SubGrpcsubg 17852  Cntzccntz 18011   DProd cdprd 18659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-0g 16368  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-grp 17692  df-minusg 17693  df-subg 17855  df-cntz 18013  df-dprd 18661
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator