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 12 33 fexd ( 𝜑𝐻 ∈ V )
35 eqid ran 𝐺 = ran 𝐺
36 35 isrngo ( 𝐻 ∈ V → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
37 34 36 syl ( 𝜑 → ( ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps ↔ ( ( 𝐺 ∈ AbelOp ∧ 𝐻 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ) ∧ ( ∀ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺𝑧 ∈ ran 𝐺 ( ( ( 𝑥 𝐻 𝑦 ) 𝐻 𝑧 ) = ( 𝑥 𝐻 ( 𝑦 𝐻 𝑧 ) ) ∧ ( 𝑥 𝐻 ( 𝑦 𝐺 𝑧 ) ) = ( ( 𝑥 𝐻 𝑦 ) 𝐺 ( 𝑥 𝐻 𝑧 ) ) ∧ ( ( 𝑥 𝐺 𝑦 ) 𝐻 𝑧 ) = ( ( 𝑥 𝐻 𝑧 ) 𝐺 ( 𝑦 𝐻 𝑧 ) ) ) ∧ ∃ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺 ( ( 𝑥 𝐻 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐻 𝑥 ) = 𝑦 ) ) ) ) )
38 30 37 mpbird ( 𝜑 → ⟨ 𝐺 , 𝐻 ⟩ ∈ RingOps )