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

Theorem opprdomnbg 13754
Description: A class is a domain if and only if its opposite is a domain, biconditional form of opprdomn 13755. (Contributed by SN, 15-Jun-2015.)
Hypothesis
Ref Expression
opprdomn.1 𝑂 = (oppr𝑅)
Assertion
Ref Expression
opprdomnbg (𝑅𝑉 → (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn))

Proof of Theorem opprdomnbg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opprdomn.1 . . . 4 𝑂 = (oppr𝑅)
21opprnzrbg 13665 . . 3 (𝑅𝑉 → (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing))
3 eqid 2193 . . . . . 6 (Base‘𝑅) = (Base‘𝑅)
41, 3opprbasg 13555 . . . . 5 (𝑅𝑉 → (Base‘𝑅) = (Base‘𝑂))
5 vex 2763 . . . . . . . . . 10 𝑦 ∈ V
6 vex 2763 . . . . . . . . . 10 𝑥 ∈ V
7 eqid 2193 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
8 eqid 2193 . . . . . . . . . . 11 (.r𝑂) = (.r𝑂)
93, 7, 1, 8opprmulg 13551 . . . . . . . . . 10 ((𝑅𝑉𝑦 ∈ V ∧ 𝑥 ∈ V) → (𝑦(.r𝑂)𝑥) = (𝑥(.r𝑅)𝑦))
105, 6, 9mp3an23 1340 . . . . . . . . 9 (𝑅𝑉 → (𝑦(.r𝑂)𝑥) = (𝑥(.r𝑅)𝑦))
1110eqcomd 2199 . . . . . . . 8 (𝑅𝑉 → (𝑥(.r𝑅)𝑦) = (𝑦(.r𝑂)𝑥))
12 eqid 2193 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
131, 12oppr0g 13561 . . . . . . . 8 (𝑅𝑉 → (0g𝑅) = (0g𝑂))
1411, 13eqeq12d 2208 . . . . . . 7 (𝑅𝑉 → ((𝑥(.r𝑅)𝑦) = (0g𝑅) ↔ (𝑦(.r𝑂)𝑥) = (0g𝑂)))
1513eqeq2d 2205 . . . . . . . . 9 (𝑅𝑉 → (𝑥 = (0g𝑅) ↔ 𝑥 = (0g𝑂)))
1613eqeq2d 2205 . . . . . . . . 9 (𝑅𝑉 → (𝑦 = (0g𝑅) ↔ 𝑦 = (0g𝑂)))
1715, 16orbi12d 794 . . . . . . . 8 (𝑅𝑉 → ((𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅)) ↔ (𝑥 = (0g𝑂) ∨ 𝑦 = (0g𝑂))))
18 orcom 729 . . . . . . . 8 ((𝑥 = (0g𝑂) ∨ 𝑦 = (0g𝑂)) ↔ (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))
1917, 18bitrdi 196 . . . . . . 7 (𝑅𝑉 → ((𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅)) ↔ (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂))))
2014, 19imbi12d 234 . . . . . 6 (𝑅𝑉 → (((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅))) ↔ ((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))))
214, 20raleqbidv 2706 . . . . 5 (𝑅𝑉 → (∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅))) ↔ ∀𝑦 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))))
224, 21raleqbidv 2706 . . . 4 (𝑅𝑉 → (∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅))) ↔ ∀𝑥 ∈ (Base‘𝑂)∀𝑦 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))))
23 ralcom 2657 . . . 4 (∀𝑥 ∈ (Base‘𝑂)∀𝑦 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂))) ↔ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂))))
2422, 23bitrdi 196 . . 3 (𝑅𝑉 → (∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅))) ↔ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))))
252, 24anbi12d 473 . 2 (𝑅𝑉 → ((𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅)))) ↔ (𝑂 ∈ NzRing ∧ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂))))))
263, 7, 12isdomn 13749 . 2 (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)((𝑥(.r𝑅)𝑦) = (0g𝑅) → (𝑥 = (0g𝑅) ∨ 𝑦 = (0g𝑅)))))
27 eqid 2193 . . 3 (Base‘𝑂) = (Base‘𝑂)
28 eqid 2193 . . 3 (0g𝑂) = (0g𝑂)
2927, 8, 28isdomn 13749 . 2 (𝑂 ∈ Domn ↔ (𝑂 ∈ NzRing ∧ ∀𝑦 ∈ (Base‘𝑂)∀𝑥 ∈ (Base‘𝑂)((𝑦(.r𝑂)𝑥) = (0g𝑂) → (𝑦 = (0g𝑂) ∨ 𝑥 = (0g𝑂)))))
3025, 26, 293bitr4g 223 1 (𝑅𝑉 → (𝑅 ∈ Domn ↔ 𝑂 ∈ Domn))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wo 709   = wceq 1364  wcel 2164  wral 2472  Vcvv 2760  cfv 5246  (class class class)co 5910  Basecbs 12608  .rcmulr 12686  0gc0g 12857  opprcoppr 13547  NzRingcnzr 13659  Domncdomn 13736
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-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-addcom 7962  ax-addass 7964  ax-i2m1 7967  ax-0lt1 7968  ax-0id 7970  ax-rnegex 7971  ax-pre-ltirr 7974  ax-pre-lttrn 7976  ax-pre-ltadd 7978
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4322  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-tpos 6289  df-pnf 8046  df-mnf 8047  df-ltxr 8049  df-inn 8973  df-2 9031  df-3 9032  df-ndx 12611  df-slot 12612  df-base 12614  df-sets 12615  df-plusg 12698  df-mulr 12699  df-0g 12859  df-mgm 12929  df-sgrp 12975  df-mnd 12988  df-grp 13065  df-mgp 13401  df-ur 13440  df-ring 13478  df-oppr 13548  df-nzr 13660  df-domn 13739
This theorem is referenced by:  opprdomn  13755
  Copyright terms: Public domain W3C validator