Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isrngo Structured version   Visualization version   GIF version

Theorem isrngo 33928
Description: The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
isring.1 𝑋 = ran 𝐺
Assertion
Ref Expression
isrngo (𝐻𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐺   𝑥,𝐻,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)

Proof of Theorem isrngo
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 4761 . . . 4 (𝐺RingOps𝐻 ↔ ⟨𝐺, 𝐻⟩ ∈ RingOps)
2 relrngo 33927 . . . . 5 Rel RingOps
32brrelexi 5267 . . . 4 (𝐺RingOps𝐻𝐺 ∈ V)
41, 3sylbir 225 . . 3 (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ V)
54a1i 11 . 2 (𝐻𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps → 𝐺 ∈ V))
6 elex 3316 . . . 4 (𝐺 ∈ AbelOp → 𝐺 ∈ V)
76ad2antrr 764 . . 3 (((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) → 𝐺 ∈ V)
87a1i 11 . 2 (𝐻𝐴 → (((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))) → 𝐺 ∈ V))
9 df-rngo 33926 . . . . 5 RingOps = {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))}
109eleq2i 2795 . . . 4 (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ⟨𝐺, 𝐻⟩ ∈ {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))})
11 simpl 474 . . . . . . . 8 ((𝑔 = 𝐺 = 𝐻) → 𝑔 = 𝐺)
1211eleq1d 2788 . . . . . . 7 ((𝑔 = 𝐺 = 𝐻) → (𝑔 ∈ AbelOp ↔ 𝐺 ∈ AbelOp))
13 simpr 479 . . . . . . . 8 ((𝑔 = 𝐺 = 𝐻) → = 𝐻)
1411rneqd 5460 . . . . . . . . . 10 ((𝑔 = 𝐺 = 𝐻) → ran 𝑔 = ran 𝐺)
15 isring.1 . . . . . . . . . 10 𝑋 = ran 𝐺
1614, 15syl6eqr 2776 . . . . . . . . 9 ((𝑔 = 𝐺 = 𝐻) → ran 𝑔 = 𝑋)
1716sqxpeqd 5250 . . . . . . . 8 ((𝑔 = 𝐺 = 𝐻) → (ran 𝑔 × ran 𝑔) = (𝑋 × 𝑋))
1813, 17, 16feq123d 6147 . . . . . . 7 ((𝑔 = 𝐺 = 𝐻) → (:(ran 𝑔 × ran 𝑔)⟶ran 𝑔𝐻:(𝑋 × 𝑋)⟶𝑋))
1912, 18anbi12d 749 . . . . . 6 ((𝑔 = 𝐺 = 𝐻) → ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ↔ (𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋)))
2013oveqd 6782 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → (𝑥𝑦) = (𝑥𝐻𝑦))
21 eqidd 2725 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → 𝑧 = 𝑧)
2213, 20, 21oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → ((𝑥𝑦)𝑧) = ((𝑥𝐻𝑦)𝐻𝑧))
23 eqidd 2725 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → 𝑥 = 𝑥)
2413oveqd 6782 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → (𝑦𝑧) = (𝑦𝐻𝑧))
2513, 23, 24oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → (𝑥(𝑦𝑧)) = (𝑥𝐻(𝑦𝐻𝑧)))
2622, 25eqeq12d 2739 . . . . . . . . . . 11 ((𝑔 = 𝐺 = 𝐻) → (((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ↔ ((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧))))
2711oveqd 6782 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
2813, 23, 27oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → (𝑥(𝑦𝑔𝑧)) = (𝑥𝐻(𝑦𝐺𝑧)))
2913oveqd 6782 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → (𝑥𝑧) = (𝑥𝐻𝑧))
3011, 20, 29oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → ((𝑥𝑦)𝑔(𝑥𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)))
3128, 30eqeq12d 2739 . . . . . . . . . . 11 ((𝑔 = 𝐺 = 𝐻) → ((𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ↔ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧))))
3211oveqd 6782 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 = 𝐻) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
3313, 32, 21oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → ((𝑥𝑔𝑦)𝑧) = ((𝑥𝐺𝑦)𝐻𝑧))
3411, 29, 24oveq123d 6786 . . . . . . . . . . . 12 ((𝑔 = 𝐺 = 𝐻) → ((𝑥𝑧)𝑔(𝑦𝑧)) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))
3533, 34eqeq12d 2739 . . . . . . . . . . 11 ((𝑔 = 𝐺 = 𝐻) → (((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧)) ↔ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))))
3626, 31, 353anbi123d 1512 . . . . . . . . . 10 ((𝑔 = 𝐺 = 𝐻) → ((((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ↔ (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3716, 36raleqbidv 3255 . . . . . . . . 9 ((𝑔 = 𝐺 = 𝐻) → (∀𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ↔ ∀𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3816, 37raleqbidv 3255 . . . . . . . 8 ((𝑔 = 𝐺 = 𝐻) → (∀𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ↔ ∀𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3916, 38raleqbidv 3255 . . . . . . 7 ((𝑔 = 𝐺 = 𝐻) → (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ↔ ∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
4020eqeq1d 2726 . . . . . . . . . 10 ((𝑔 = 𝐺 = 𝐻) → ((𝑥𝑦) = 𝑦 ↔ (𝑥𝐻𝑦) = 𝑦))
4113oveqd 6782 . . . . . . . . . . 11 ((𝑔 = 𝐺 = 𝐻) → (𝑦𝑥) = (𝑦𝐻𝑥))
4241eqeq1d 2726 . . . . . . . . . 10 ((𝑔 = 𝐺 = 𝐻) → ((𝑦𝑥) = 𝑦 ↔ (𝑦𝐻𝑥) = 𝑦))
4340, 42anbi12d 749 . . . . . . . . 9 ((𝑔 = 𝐺 = 𝐻) → (((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦) ↔ ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
4416, 43raleqbidv 3255 . . . . . . . 8 ((𝑔 = 𝐺 = 𝐻) → (∀𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦) ↔ ∀𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
4516, 44rexeqbidv 3256 . . . . . . 7 ((𝑔 = 𝐺 = 𝐻) → (∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦) ↔ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))
4639, 45anbi12d 749 . . . . . 6 ((𝑔 = 𝐺 = 𝐻) → ((∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)) ↔ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))
4719, 46anbi12d 749 . . . . 5 ((𝑔 = 𝐺 = 𝐻) → (((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦))) ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
4847opelopabga 5092 . . . 4 ((𝐺 ∈ V ∧ 𝐻𝐴) → (⟨𝐺, 𝐻⟩ ∈ {⟨𝑔, ⟩ ∣ ((𝑔 ∈ AbelOp ∧ :(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔𝑧 ∈ ran 𝑔(((𝑥𝑦)𝑧) = (𝑥(𝑦𝑧)) ∧ (𝑥(𝑦𝑔𝑧)) = ((𝑥𝑦)𝑔(𝑥𝑧)) ∧ ((𝑥𝑔𝑦)𝑧) = ((𝑥𝑧)𝑔(𝑦𝑧))) ∧ ∃𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑥𝑦) = 𝑦 ∧ (𝑦𝑥) = 𝑦)))} ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
4910, 48syl5bb 272 . . 3 ((𝐺 ∈ V ∧ 𝐻𝐴) → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
5049expcom 450 . 2 (𝐻𝐴 → (𝐺 ∈ V → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦))))))
515, 8, 50pm5.21ndd 368 1 (𝐻𝐴 → (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 × 𝑋)⟶𝑋) ∧ (∀𝑥𝑋𝑦𝑋𝑧𝑋 (((𝑥𝐻𝑦)𝐻𝑧) = (𝑥𝐻(𝑦𝐻𝑧)) ∧ (𝑥𝐻(𝑦𝐺𝑧)) = ((𝑥𝐻𝑦)𝐺(𝑥𝐻𝑧)) ∧ ((𝑥𝐺𝑦)𝐻𝑧) = ((𝑥𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑥𝐻𝑦) = 𝑦 ∧ (𝑦𝐻𝑥) = 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wral 3014  wrex 3015  Vcvv 3304  cop 4291   class class class wbr 4760  {copab 4820   × cxp 5216  ran crn 5219  wf 5997  (class class class)co 6765  AbelOpcablo 27628  RingOpscrngo 33925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-fv 6009  df-ov 6768  df-rngo 33926
This theorem is referenced by:  isrngod  33929  rngoi  33930
  Copyright terms: Public domain W3C validator