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 36813
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 5150 . . . 4 (𝐺RingOps𝐻 ↔ ⟨𝐺, 𝐻⟩ ∈ RingOps)
2 relrngo 36812 . . . . 5 Rel RingOps
32brrelex1i 5733 . . . 4 (𝐺RingOps𝐻 β†’ 𝐺 ∈ V)
41, 3sylbir 234 . . 3 (⟨𝐺, 𝐻⟩ ∈ RingOps β†’ 𝐺 ∈ V)
54a1i 11 . 2 (𝐻 ∈ 𝐴 β†’ (⟨𝐺, 𝐻⟩ ∈ RingOps β†’ 𝐺 ∈ V))
6 elex 3493 . . . 4 (𝐺 ∈ AbelOp β†’ 𝐺 ∈ V)
76ad2antrr 725 . . 3 (((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦))) β†’ 𝐺 ∈ V)
87a1i 11 . 2 (𝐻 ∈ 𝐴 β†’ (((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦))) β†’ 𝐺 ∈ V))
9 df-rngo 36811 . . . . 5 RingOps = {βŸ¨π‘”, β„ŽβŸ© ∣ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)))}
109eleq2i 2826 . . . 4 (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ⟨𝐺, 𝐻⟩ ∈ {βŸ¨π‘”, β„ŽβŸ© ∣ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)))})
11 simpl 484 . . . . . . . 8 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ 𝑔 = 𝐺)
1211eleq1d 2819 . . . . . . 7 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (𝑔 ∈ AbelOp ↔ 𝐺 ∈ AbelOp))
13 simpr 486 . . . . . . . 8 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ β„Ž = 𝐻)
1411rneqd 5938 . . . . . . . . . 10 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ran 𝑔 = ran 𝐺)
15 isring.1 . . . . . . . . . 10 𝑋 = ran 𝐺
1614, 15eqtr4di 2791 . . . . . . . . 9 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ran 𝑔 = 𝑋)
1716sqxpeqd 5709 . . . . . . . 8 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (ran 𝑔 Γ— ran 𝑔) = (𝑋 Γ— 𝑋))
1813, 17, 16feq123d 6707 . . . . . . 7 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔 ↔ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹))
1912, 18anbi12d 632 . . . . . 6 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ↔ (𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹)))
2013oveqd 7426 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘₯β„Žπ‘¦) = (π‘₯𝐻𝑦))
21 eqidd 2734 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ 𝑧 = 𝑧)
2213, 20, 21oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯β„Žπ‘¦)β„Žπ‘§) = ((π‘₯𝐻𝑦)𝐻𝑧))
23 eqidd 2734 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ π‘₯ = π‘₯)
2413oveqd 7426 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘¦β„Žπ‘§) = (𝑦𝐻𝑧))
2513, 23, 24oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘₯β„Ž(π‘¦β„Žπ‘§)) = (π‘₯𝐻(𝑦𝐻𝑧)))
2622, 25eqeq12d 2749 . . . . . . . . . . 11 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ↔ ((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧))))
2711oveqd 7426 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
2813, 23, 27oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘₯β„Ž(𝑦𝑔𝑧)) = (π‘₯𝐻(𝑦𝐺𝑧)))
2913oveqd 7426 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘₯β„Žπ‘§) = (π‘₯𝐻𝑧))
3011, 20, 29oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)))
3128, 30eqeq12d 2749 . . . . . . . . . . 11 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ↔ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧))))
3211oveqd 7426 . . . . . . . . . . . . 13 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘₯𝑔𝑦) = (π‘₯𝐺𝑦))
3313, 32, 21oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯𝐺𝑦)𝐻𝑧))
3411, 29, 24oveq123d 7430 . . . . . . . . . . . 12 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧)))
3533, 34eqeq12d 2749 . . . . . . . . . . 11 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§)) ↔ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))))
3626, 31, 353anbi123d 1437 . . . . . . . . . 10 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ↔ (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3716, 36raleqbidv 3343 . . . . . . . . 9 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ↔ βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3816, 37raleqbidv 3343 . . . . . . . 8 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ↔ βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
3916, 38raleqbidv 3343 . . . . . . 7 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ↔ βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧)))))
4020eqeq1d 2735 . . . . . . . . . 10 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘₯β„Žπ‘¦) = 𝑦 ↔ (π‘₯𝐻𝑦) = 𝑦))
4113oveqd 7426 . . . . . . . . . . 11 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (π‘¦β„Žπ‘₯) = (𝑦𝐻π‘₯))
4241eqeq1d 2735 . . . . . . . . . 10 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((π‘¦β„Žπ‘₯) = 𝑦 ↔ (𝑦𝐻π‘₯) = 𝑦))
4340, 42anbi12d 632 . . . . . . . . 9 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦) ↔ ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))
4416, 43raleqbidv 3343 . . . . . . . 8 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦) ↔ βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))
4516, 44rexeqbidv 3344 . . . . . . 7 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦) ↔ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))
4639, 45anbi12d 632 . . . . . 6 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ ((βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)) ↔ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦))))
4719, 46anbi12d 632 . . . . 5 ((𝑔 = 𝐺 ∧ β„Ž = 𝐻) β†’ (((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦))) ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))))
4847opelopabga 5534 . . . 4 ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) β†’ (⟨𝐺, 𝐻⟩ ∈ {βŸ¨π‘”, β„ŽβŸ© ∣ ((𝑔 ∈ AbelOp ∧ β„Ž:(ran 𝑔 Γ— ran 𝑔)⟢ran 𝑔) ∧ (βˆ€π‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran π‘”βˆ€π‘§ ∈ ran 𝑔(((π‘₯β„Žπ‘¦)β„Žπ‘§) = (π‘₯β„Ž(π‘¦β„Žπ‘§)) ∧ (π‘₯β„Ž(𝑦𝑔𝑧)) = ((π‘₯β„Žπ‘¦)𝑔(π‘₯β„Žπ‘§)) ∧ ((π‘₯𝑔𝑦)β„Žπ‘§) = ((π‘₯β„Žπ‘§)𝑔(π‘¦β„Žπ‘§))) ∧ βˆƒπ‘₯ ∈ ran π‘”βˆ€π‘¦ ∈ ran 𝑔((π‘₯β„Žπ‘¦) = 𝑦 ∧ (π‘¦β„Žπ‘₯) = 𝑦)))} ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))))
4910, 48bitrid 283 . . 3 ((𝐺 ∈ V ∧ 𝐻 ∈ 𝐴) β†’ (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))))
5049expcom 415 . 2 (𝐻 ∈ 𝐴 β†’ (𝐺 ∈ V β†’ (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦))))))
515, 8, 50pm5.21ndd 381 1 (𝐻 ∈ 𝐴 β†’ (⟨𝐺, 𝐻⟩ ∈ RingOps ↔ ((𝐺 ∈ AbelOp ∧ 𝐻:(𝑋 Γ— 𝑋)βŸΆπ‘‹) ∧ (βˆ€π‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 βˆ€π‘§ ∈ 𝑋 (((π‘₯𝐻𝑦)𝐻𝑧) = (π‘₯𝐻(𝑦𝐻𝑧)) ∧ (π‘₯𝐻(𝑦𝐺𝑧)) = ((π‘₯𝐻𝑦)𝐺(π‘₯𝐻𝑧)) ∧ ((π‘₯𝐺𝑦)𝐻𝑧) = ((π‘₯𝐻𝑧)𝐺(𝑦𝐻𝑧))) ∧ βˆƒπ‘₯ ∈ 𝑋 βˆ€π‘¦ ∈ 𝑋 ((π‘₯𝐻𝑦) = 𝑦 ∧ (𝑦𝐻π‘₯) = 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475  βŸ¨cop 4635   class class class wbr 5149  {copab 5211   Γ— cxp 5675  ran crn 5678  βŸΆwf 6540  (class class class)co 7409  AbelOpcablo 29828  RingOpscrngo 36810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-rngo 36811
This theorem is referenced by:  isrngod  36814  rngoi  36815
  Copyright terms: Public domain W3C validator