Metamath Proof Explorer

Theorem iscringd

Description: Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses iscringd.1 ⊢ ( 𝜑 → 𝐺 ∈ AbelOp )
iscringd.2 ⊢ ( 𝜑 → 𝑋 = ran 𝐺 )
iscringd.3 ⊢ ( 𝜑 → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
iscringd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
iscringd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) )
iscringd.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
iscringd.7 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝐻 𝑈 ) = 𝑦 )
iscringd.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
Assertion iscringd ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ CRingOps )

Proof

Step Hyp Ref Expression
1 iscringd.1 ⊢ ( 𝜑 → 𝐺 ∈ AbelOp )
2 iscringd.2 ⊢ ( 𝜑 → 𝑋 = ran 𝐺 )
3 iscringd.3 ⊢ ( 𝜑 → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
4 iscringd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
5 iscringd.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) )
6 iscringd.6 ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
7 iscringd.7 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝐻 𝑈 ) = 𝑦 )
8 iscringd.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
9 id ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) )
10 9 3com13 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) )
11 eleq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑋 ↔ 𝑧 ∈ 𝑋 ) )
12 11 3anbi1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) )
13 12 anbi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) ) )
14 oveq2 ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) )
15 oveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 𝐻 𝑤 ) = ( 𝑥 𝐻 𝑧 ) )
16 oveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 𝐻 𝑤 ) = ( 𝑦 𝐻 𝑧 ) )
17 15 16 oveq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
18 14 17 eqeq12d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
19 13 18 imbi12d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
20 eleq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑋 ↔ 𝑥 ∈ 𝑋 ) )
21 20 3anbi3d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ↔ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) )
22 21 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) ) )
23 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐺 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
24 23 oveq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) )
25 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐻 𝑤 ) = ( 𝑥 𝐻 𝑤 ) )
26 25 oveq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) )
27 24 26 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) )
28 22 27 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) ) )
29 eleq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋 ) )
30 29 3anbi1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ↔ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) )
31 30 anbi2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ) )
32 oveq2 ⊢ ( 𝑥 = 𝑤 → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑥 ) = ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) )
33 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 𝐻 𝑥 ) = ( 𝑧 𝐻 𝑤 ) )
34 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑤 ) )
35 33 34 oveq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) )
36 32 35 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑥 ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) ↔ ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) )
37 31 36 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑥 ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) ) ) )
38 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝐺 ∈ AbelOp )
39 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
40 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑋 = ran 𝐺 )
41 39 40 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ ran 𝐺 )
42 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
43 42 40 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ ran 𝐺 )
44 eqid ⊢ ran 𝐺 = ran 𝐺
45 44 ablocom ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝑧 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑧 ) )
46 38 41 43 45 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑧 ) )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑥 ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) )
48 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
49 ablogrpo ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
50 38 49 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝐺 ∈ GrpOp )
51 44 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ ran 𝐺 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐺 𝑧 ) ∈ ran 𝐺 )
52 50 43 41 51 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝐺 𝑧 ) ∈ ran 𝐺 )
53 52 40 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 )
54 48 53 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) )
55 ovex ⊢ ( 𝑦 𝐺 𝑧 ) ∈ V
56 eleq1 ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( 𝑤 ∈ 𝑋 ↔ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) )
57 56 anbi2d ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) ) )
58 57 anbi2d ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) ) ) )
59 oveq2 ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( 𝑥 𝐻 𝑤 ) = ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) )
60 oveq1 ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( 𝑤 𝐻 𝑥 ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) )
61 59 60 eqeq12d ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( ( 𝑥 𝐻 𝑤 ) = ( 𝑤 𝐻 𝑥 ) ↔ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) ) )
62 58 61 imbi12d ⊢ ( 𝑤 = ( 𝑦 𝐺 𝑧 ) → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑤 ) = ( 𝑤 𝐻 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) ) ) )
63 eleq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑋 ↔ 𝑤 ∈ 𝑋 ) )
64 63 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) )
65 64 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ) )
66 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑤 ) )
67 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝐻 𝑥 ) = ( 𝑤 𝐻 𝑥 ) )
68 66 67 eqeq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ( 𝑥 𝐻 𝑤 ) = ( 𝑤 𝐻 𝑥 ) ) )
69 65 68 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑤 ) = ( 𝑤 𝐻 𝑥 ) ) ) )
70 69 8 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑤 ) = ( 𝑤 𝐻 𝑥 ) )
71 55 62 70 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐺 𝑧 ) ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) )
72 54 71 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑦 𝐺 𝑧 ) 𝐻 𝑥 ) )
73 8 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
74 eleq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑋 ↔ 𝑧 ∈ 𝑋 ) )
75 74 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) )
76 75 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) ) )
77 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑧 ) )
78 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝐻 𝑥 ) = ( 𝑧 𝐻 𝑥 ) )
79 77 78 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ( 𝑥 𝐻 𝑧 ) = ( 𝑧 𝐻 𝑥 ) ) )
80 76 79 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑧 𝐻 𝑥 ) ) ) )
81 80 8 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑧 𝐻 𝑥 ) )
82 81 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑧 𝐻 𝑥 ) )
83 73 82 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) = ( ( 𝑦 𝐻 𝑥 ) 𝐺 ( 𝑧 𝐻 𝑥 ) ) )
84 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
85 84 42 48 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝐻 𝑥 ) ∈ 𝑋 )
86 85 40 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 𝐻 𝑥 ) ∈ ran 𝐺 )
87 84 39 48 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐻 𝑥 ) ∈ 𝑋 )
88 87 40 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 𝐻 𝑥 ) ∈ ran 𝐺 )
89 44 ablocom ⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝑦 𝐻 𝑥 ) ∈ ran 𝐺 ∧ ( 𝑧 𝐻 𝑥 ) ∈ ran 𝐺 ) → ( ( 𝑦 𝐻 𝑥 ) 𝐺 ( 𝑧 𝐻 𝑥 ) ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) )
90 38 86 88 89 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 𝐻 𝑥 ) 𝐺 ( 𝑧 𝐻 𝑥 ) ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) )
91 5 83 90 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) )
92 47 72 91 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑥 ) = ( ( 𝑧 𝐻 𝑥 ) 𝐺 ( 𝑦 𝐻 𝑥 ) ) )
93 37 92 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑧 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) )
94 28 93 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑤 ) = ( ( 𝑥 𝐻 𝑤 ) 𝐺 ( 𝑦 𝐻 𝑤 ) ) )
95 19 94 chvarvv ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
96 10 95 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
97 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑈 ∈ 𝑋 )
98 oveq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 𝐻 𝑦 ) = ( 𝑈 𝐻 𝑦 ) )
99 oveq2 ⊢ ( 𝑥 = 𝑈 → ( 𝑦 𝐻 𝑥 ) = ( 𝑦 𝐻 𝑈 ) )
100 98 99 eqeq12d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ↔ ( 𝑈 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑈 ) ) )
101 100 imbi2d ⊢ ( 𝑥 = 𝑈 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑈 ) ) ) )
102 8 an12s ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
103 102 ex ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
104 101 103 vtoclga ⊢ ( 𝑈 ∈ 𝑋 → ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑈 ) ) )
105 97 104 mpcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑈 ) )
106 105 7 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑦 ) = 𝑦 )
107 1 2 3 4 5 96 6 106 7 isrngod ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )
108 2 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ran 𝐺 ) )
109 2 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ran 𝐺 ) )
110 108 109 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) )
111 110 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
112 111 8 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
113 112 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) )
114 rnexg ⊢ ( 𝐺 ∈ AbelOp → ran 𝐺 ∈ V )
115 1 114 syl ⊢ ( 𝜑 → ran 𝐺 ∈ V )
116 2 115 eqeltrd ⊢ ( 𝜑 → 𝑋 ∈ V )
117 116 116 xpexd ⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) ∈ V )
118 fex ⊢ ( ( 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ( 𝑋 × 𝑋 ) ∈ V ) → 𝐻 ∈ V )
119 3 117 118 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
120 iscom2 ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 ∈ V ) → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
121 1 119 120 syl2anc ⊢ ( 𝜑 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( 𝑥 𝐻 𝑦 ) = ( 𝑦 𝐻 𝑥 ) ) )
122 113 121 mpbird ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 )
123 iscrngo ⊢ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ CRingOps ↔ ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ∧ ⟨ 𝐺 , 𝐻 ⟩ ∈ Com2 ) )
124 107 122 123 sylanbrc ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ CRingOps )