This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isrngo

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.)

Ref Expression
Hypothesis isring.1 ⊢ 𝑋 = ran 𝐺
Assertion isrngo ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isring.1 ⊢ 𝑋 = ran 𝐺
2 df-br ⊢ ( 𝐺 RingOps 𝐻 ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )
3 relrngo ⊢ Rel RingOps
4 3 brrelex1i ⊢ ( 𝐺 RingOps 𝐻 → 𝐺 ∈ V )
5 2 4 sylbir ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ V )
6 5 a1i ⊢ ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps → 𝐺 ∈ V ) )
7 elex ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ V )
8 7 ad2antrr ⊢ ( ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) → 𝐺 ∈ V )
9 8 a1i ⊢ ( 𝐻 ∈ 𝐴 → ( ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) → 𝐺 ∈ V ) )
10 df-rngo ⊢ RingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) }
11 10 eleq2i ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) } )
12 simpl ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → 𝑔 = 𝐺 )
13 12 eleq1d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑔 ∈ AbelOp ↔ 𝐺 ∈ AbelOp ) )
14 simpr ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
15 12 rneqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ran 𝑔 = ran 𝐺 )
16 15 1 eqtr4di ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ran 𝑔 = 𝑋 )
17 16 sqxpeqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ran 𝑔 × ran 𝑔 ) = ( 𝑋 × 𝑋 ) )
18 14 17 16 feq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ↔ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
19 13 18 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ↔ ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ) )
20 14 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
21 eqidd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → 𝑧 = 𝑧 )
22 14 20 21 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) )
23 eqidd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → 𝑥 = 𝑥 )
24 14 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑦 ℎ 𝑧 ) = ( 𝑦 𝐻 𝑧 ) )
25 14 23 24 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
26 22 25 eqeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ↔ ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ) )
27 12 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑦 𝑔 𝑧 ) = ( 𝑦 𝐺 𝑧 ) )
28 14 23 27 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) )
29 14 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑥 ℎ 𝑧 ) = ( 𝑥 𝐻 𝑧 ) )
30 12 20 29 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) )
31 28 30 eqeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ↔ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ) )
32 12 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
33 14 32 21 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) )
34 12 29 24 oveq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
35 33 34 eqeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
36 26 31 35 3anbi123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ↔ ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
37 16 36 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
38 16 37 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
39 16 38 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
40 20 eqeq1d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) = 𝑦 ) )
41 14 oveqd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑦 ℎ 𝑥 ) = ( 𝑦 𝐻 𝑥 ) )
42 41 eqeq1d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑦 ℎ 𝑥 ) = 𝑦 ↔ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
43 40 42 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
44 16 43 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
45 16 44 rexeqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
46 39 45 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
47 19 46 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
48 47 opelopabga ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( 𝑔 ∈ AbelOp ∧ ℎ : ( ran 𝑔 × ran 𝑔 ) ⟶ ran 𝑔 ) ∧ ( ∀ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ∀ 𝑧 ∈ ran 𝑔 ( ( ( 𝑥 ℎ 𝑦 ) ℎ 𝑧 ) = ( 𝑥 ℎ ( 𝑦 ℎ 𝑧 ) ) ∧ ( 𝑥 ℎ ( 𝑦 𝑔 𝑧 ) ) = ( ( 𝑥 ℎ 𝑦 ) 𝑔 ( 𝑥 ℎ 𝑧 ) ) ∧ ( ( 𝑥 𝑔 𝑦 ) ℎ 𝑧 ) = ( ( 𝑥 ℎ 𝑧 ) 𝑔 ( 𝑦 ℎ 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝑔 ∀ 𝑦 ∈ ran 𝑔 ( ( 𝑥 ℎ 𝑦 ) = 𝑦 ∧ ( 𝑦 ℎ 𝑥 ) = 𝑦 ) ) ) } ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
49 11 48 bitrid ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ 𝐴 ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
50 49 expcom ⊢ ( 𝐻 ∈ 𝐴 → ( 𝐺 ∈ V → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) ) )
51 6 9 50 pm5.21ndd ⊢ ( 𝐻 ∈ 𝐴 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )