ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  grppropd GIF version

Theorem grppropd 12892
Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
grppropd.1 (𝜑𝐵 = (Base‘𝐾))
grppropd.2 (𝜑𝐵 = (Base‘𝐿))
grppropd.3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
Assertion
Ref Expression
grppropd (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝜑,𝑥,𝑦

Proof of Theorem grppropd
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grppropd.1 . . . 4 (𝜑𝐵 = (Base‘𝐾))
2 grppropd.2 . . . 4 (𝜑𝐵 = (Base‘𝐿))
3 grppropd.3 . . . 4 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
41, 2, 3mndpropd 12840 . . 3 (𝜑 → (𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd))
51adantr 276 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐵 = (Base‘𝐾))
62adantr 276 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐵 = (Base‘𝐿))
7 simprl 529 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
85, 7basmexd 12521 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐾 ∈ V)
96, 7basmexd 12521 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐿 ∈ V)
103ralrimivva 2559 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))
11 oveq1 5881 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑥(+g𝐾)𝑦) = (𝑧(+g𝐾)𝑦))
12 oveq1 5881 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (𝑥(+g𝐿)𝑦) = (𝑧(+g𝐿)𝑦))
1311, 12eqeq12d 2192 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧 → ((𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦) ↔ (𝑧(+g𝐾)𝑦) = (𝑧(+g𝐿)𝑦)))
14 oveq2 5882 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑧(+g𝐾)𝑦) = (𝑧(+g𝐾)𝑤))
15 oveq2 5882 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑤 → (𝑧(+g𝐿)𝑦) = (𝑧(+g𝐿)𝑤))
1614, 15eqeq12d 2192 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤 → ((𝑧(+g𝐾)𝑦) = (𝑧(+g𝐿)𝑦) ↔ (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤)))
1713, 16cbvral2v 2716 . . . . . . . . . . . . . 14 (∀𝑥𝐵𝑦𝐵 (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦) ↔ ∀𝑧𝐵𝑤𝐵 (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
1810, 17sylib 122 . . . . . . . . . . . . 13 (𝜑 → ∀𝑧𝐵𝑤𝐵 (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
1918adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ∀𝑧𝐵𝑤𝐵 (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
2019r19.21bi 2565 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑧𝐵) → ∀𝑤𝐵 (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
2120r19.21bi 2565 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑧𝐵) ∧ 𝑤𝐵) → (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
2221anasss 399 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(+g𝐾)𝑤) = (𝑧(+g𝐿)𝑤))
235, 6, 8, 9, 22grpidpropdg 12792 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (0g𝐾) = (0g𝐿))
243, 23eqeq12d 2192 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ (𝑥(+g𝐿)𝑦) = (0g𝐿)))
2524anass1rs 571 . . . . . 6 (((𝜑𝑦𝐵) ∧ 𝑥𝐵) → ((𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ (𝑥(+g𝐿)𝑦) = (0g𝐿)))
2625rexbidva 2474 . . . . 5 ((𝜑𝑦𝐵) → (∃𝑥𝐵 (𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ ∃𝑥𝐵 (𝑥(+g𝐿)𝑦) = (0g𝐿)))
2726ralbidva 2473 . . . 4 (𝜑 → (∀𝑦𝐵𝑥𝐵 (𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ ∀𝑦𝐵𝑥𝐵 (𝑥(+g𝐿)𝑦) = (0g𝐿)))
281rexeqdv 2679 . . . . 5 (𝜑 → (∃𝑥𝐵 (𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ ∃𝑥 ∈ (Base‘𝐾)(𝑥(+g𝐾)𝑦) = (0g𝐾)))
291, 28raleqbidv 2684 . . . 4 (𝜑 → (∀𝑦𝐵𝑥𝐵 (𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ ∀𝑦 ∈ (Base‘𝐾)∃𝑥 ∈ (Base‘𝐾)(𝑥(+g𝐾)𝑦) = (0g𝐾)))
302rexeqdv 2679 . . . . 5 (𝜑 → (∃𝑥𝐵 (𝑥(+g𝐿)𝑦) = (0g𝐿) ↔ ∃𝑥 ∈ (Base‘𝐿)(𝑥(+g𝐿)𝑦) = (0g𝐿)))
312, 30raleqbidv 2684 . . . 4 (𝜑 → (∀𝑦𝐵𝑥𝐵 (𝑥(+g𝐿)𝑦) = (0g𝐿) ↔ ∀𝑦 ∈ (Base‘𝐿)∃𝑥 ∈ (Base‘𝐿)(𝑥(+g𝐿)𝑦) = (0g𝐿)))
3227, 29, 313bitr3d 218 . . 3 (𝜑 → (∀𝑦 ∈ (Base‘𝐾)∃𝑥 ∈ (Base‘𝐾)(𝑥(+g𝐾)𝑦) = (0g𝐾) ↔ ∀𝑦 ∈ (Base‘𝐿)∃𝑥 ∈ (Base‘𝐿)(𝑥(+g𝐿)𝑦) = (0g𝐿)))
334, 32anbi12d 473 . 2 (𝜑 → ((𝐾 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐾)∃𝑥 ∈ (Base‘𝐾)(𝑥(+g𝐾)𝑦) = (0g𝐾)) ↔ (𝐿 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐿)∃𝑥 ∈ (Base‘𝐿)(𝑥(+g𝐿)𝑦) = (0g𝐿))))
34 eqid 2177 . . 3 (Base‘𝐾) = (Base‘𝐾)
35 eqid 2177 . . 3 (+g𝐾) = (+g𝐾)
36 eqid 2177 . . 3 (0g𝐾) = (0g𝐾)
3734, 35, 36isgrp 12882 . 2 (𝐾 ∈ Grp ↔ (𝐾 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐾)∃𝑥 ∈ (Base‘𝐾)(𝑥(+g𝐾)𝑦) = (0g𝐾)))
38 eqid 2177 . . 3 (Base‘𝐿) = (Base‘𝐿)
39 eqid 2177 . . 3 (+g𝐿) = (+g𝐿)
40 eqid 2177 . . 3 (0g𝐿) = (0g𝐿)
4138, 39, 40isgrp 12882 . 2 (𝐿 ∈ Grp ↔ (𝐿 ∈ Mnd ∧ ∀𝑦 ∈ (Base‘𝐿)∃𝑥 ∈ (Base‘𝐿)(𝑥(+g𝐿)𝑦) = (0g𝐿)))
4233, 37, 413bitr4g 223 1 (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  wral 2455  wrex 2456  Vcvv 2737  cfv 5216  (class class class)co 5874  Basecbs 12461  +gcplusg 12535  0gc0g 12704  Mndcmnd 12816  Grpcgrp 12876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-iota 5178  df-fun 5218  df-fn 5219  df-fv 5224  df-riota 5830  df-ov 5877  df-inn 8919  df-2 8977  df-ndx 12464  df-slot 12465  df-base 12467  df-plusg 12548  df-0g 12706  df-mgm 12774  df-sgrp 12807  df-mnd 12817  df-grp 12879
This theorem is referenced by:  grpprop  12893  grppropstrg  12894  ablpropd  13097  ringpropd  13215  opprring  13247
  Copyright terms: Public domain W3C validator