Metamath Proof Explorer

Theorem isrngod

Description: Conditions that determine a ring. (Changed label from isringd to isrngod -NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 isringod.1 ⊢ ( 𝜑 → 𝐺 ∈ AbelOp )
2 isringod.2 ⊢ ( 𝜑 → 𝑋 = ran 𝐺 )
3 isringod.3 ⊢ ( 𝜑 → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
4 isringod.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) )
5 isringod.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) )
6 isringod.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) )
7 isringod.7 ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
8 isringod.8 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑈 𝐻 𝑦 ) = 𝑦 )
9 isringod.9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝐻 𝑈 ) = 𝑦 )
10 2 sqxpeqd ⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) = ( ran 𝐺 × ran 𝐺 ) )
11 10 2 feq23d ⊢ ( 𝜑 → ( 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) )
12 3 11 mpbid ⊢ ( 𝜑 → 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 )
13 4 5 6 3jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
14 13 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
15 2 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
16 2 15 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
17 2 16 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ) )
18 14 17 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) )
19 8 9 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑈 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑈 ) = 𝑦 ) )
20 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 ( ( 𝑈 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑈 ) = 𝑦 ) )
21 oveq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 𝐻 𝑦 ) = ( 𝑈 𝐻 𝑦 ) )
22 21 eqeq1d ⊢ ( 𝑥 = 𝑈 → ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ↔ ( 𝑈 𝐻 𝑦 ) = 𝑦 ) )
23 22 ovanraleqv ⊢ ( 𝑥 = 𝑈 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑈 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑈 ) = 𝑦 ) ) )
24 23 rspcev ⊢ ( ( 𝑈 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑈 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑈 ) = 𝑦 ) ) → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
25 7 20 24 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
26 2 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
27 2 26 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
28 25 27 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) )
29 18 28 jca ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) )
30 1 12 29 jca31 ⊢ ( 𝜑 → ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) )
31 rnexg ⊢ ( 𝐺 ∈ AbelOp → ran 𝐺 ∈ V )
32 1 31 syl ⊢ ( 𝜑 → ran 𝐺 ∈ V )
33 32 32 xpexd ⊢ ( 𝜑 → ( ran 𝐺 × ran 𝐺 ) ∈ V )
34 fex ⊢ ( ( 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ( ran 𝐺 × ran 𝐺 ) ∈ V ) → 𝐻 ∈ V )
35 12 33 34 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ V )
36 eqid ⊢ ran 𝐺 = ran 𝐺
37 36 isrngo ⊢ ( 𝐻 ∈ V → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
38 35 37 syl ⊢ ( 𝜑 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
39 30 38 mpbird ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )