Metamath Proof Explorer

Theorem isring

Description: The predicate "is a (unital) ring." Definition of ring with unit in Schechter p. 187. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses isring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isring.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
isring.p ⊢ + = ( +g ‘ 𝑅 )
isring.t ⊢ · = ( .r ‘ 𝑅 )
Assertion isring ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isring.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isring.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3 isring.p ⊢ + = ( +g ‘ 𝑅 )
4 isring.t ⊢ · = ( .r ‘ 𝑅 )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
6 5 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝐺 )
7 6 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ↔ 𝐺 ∈ Mnd ) )
8 fvexd ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
9 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
10 9 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
11 fvexd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) ∈ V )
12 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → 𝑟 = 𝑅 )
13 12 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = ( +g ‘ 𝑅 ) )
14 13 3 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( +g ‘ 𝑟 ) = + )
15 fvexd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) ∈ V )
16 simpll ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → 𝑟 = 𝑅 )
17 16 fveq2d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
18 17 4 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( .r ‘ 𝑟 ) = · )
19 simpllr ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑏 = 𝐵 )
20 simpr ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑡 = · )
21 eqidd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑥 = 𝑥 )
22 simplr ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑝 = + )
23 22 oveqd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑝 𝑧 ) = ( 𝑦 + 𝑧 ) )
24 20 21 23 oveq123d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) )
25 20 oveqd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑦 ) = ( 𝑥 · 𝑦 ) )
26 20 oveqd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑡 𝑧 ) = ( 𝑥 · 𝑧 ) )
27 22 25 26 oveq123d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
28 24 27 eqeq12d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ↔ ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ) )
29 22 oveqd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑥 𝑝 𝑦 ) = ( 𝑥 + 𝑦 ) )
30 eqidd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → 𝑧 = 𝑧 )
31 20 29 30 oveq123d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) )
32 20 oveqd ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( 𝑦 𝑡 𝑧 ) = ( 𝑦 · 𝑧 ) )
33 22 26 32 oveq123d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
34 31 33 eqeq12d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ↔ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) )
35 28 34 anbi12d ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
36 19 35 raleqbidv ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
37 19 36 raleqbidv ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
38 19 37 raleqbidv ⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) ∧ 𝑡 = · ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
39 15 18 38 sbcied2 ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) ∧ 𝑝 = + ) → ( [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
40 11 14 39 sbcied2 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = 𝐵 ) → ( [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
41 8 10 40 sbcied2 ⊢ ( 𝑟 = 𝑅 → ( [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )
42 7 41 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
43 df-ring ⊢ Ring = { 𝑟 ∈ Grp ∣ ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ [ ( Base ‘ 𝑟 ) / 𝑏 ] [ ( +g ‘ 𝑟 ) / 𝑝 ] [ ( .r ‘ 𝑟 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }
44 42 43 elrab2 ⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
45 3anass ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ↔ ( 𝑅 ∈ Grp ∧ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) ) )
46 44 45 bitr4i ⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )