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 ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) ) ) )