Metamath Proof Explorer


Theorem isrngd

Description: Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025)

Ref Expression
Hypotheses isrngd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
isrngd.p ( 𝜑+ = ( +g𝑅 ) )
isrngd.t ( 𝜑· = ( .r𝑅 ) )
isrngd.g ( 𝜑𝑅 ∈ Abel )
isrngd.c ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
isrngd.a ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
isrngd.d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
isrngd.e ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
Assertion isrngd ( 𝜑𝑅 ∈ Rng )

Proof

Step Hyp Ref Expression
1 isrngd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
2 isrngd.p ( 𝜑+ = ( +g𝑅 ) )
3 isrngd.t ( 𝜑· = ( .r𝑅 ) )
4 isrngd.g ( 𝜑𝑅 ∈ Abel )
5 isrngd.c ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
6 isrngd.a ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
7 isrngd.d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
8 isrngd.e ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
9 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
10 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 9 10 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
12 1 11 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
13 eqid ( .r𝑅 ) = ( .r𝑅 )
14 9 13 mgpplusg ( .r𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
15 3 14 eqtrdi ( 𝜑· = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
16 fvexd ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ V )
17 12 15 5 6 16 issgrpd ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Smgrp )
18 1 eleq2d ( 𝜑 → ( 𝑥𝐵𝑥 ∈ ( Base ‘ 𝑅 ) ) )
19 1 eleq2d ( 𝜑 → ( 𝑦𝐵𝑦 ∈ ( Base ‘ 𝑅 ) ) )
20 1 eleq2d ( 𝜑 → ( 𝑧𝐵𝑧 ∈ ( Base ‘ 𝑅 ) ) )
21 18 19 20 3anbi123d ( 𝜑 → ( ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) )
22 21 biimpar ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) )
23 3 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → · = ( .r𝑅 ) )
24 eqidd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → 𝑥 = 𝑥 )
25 2 oveqdr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g𝑅 ) 𝑧 ) )
26 23 24 25 oveq123d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) )
27 2 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → + = ( +g𝑅 ) )
28 3 oveqdr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r𝑅 ) 𝑦 ) )
29 3 oveqdr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 · 𝑧 ) = ( 𝑥 ( .r𝑅 ) 𝑧 ) )
30 27 28 29 oveq123d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) )
31 7 26 30 3eqtr3d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) )
32 2 oveqdr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g𝑅 ) 𝑦 ) )
33 eqidd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → 𝑧 = 𝑧 )
34 23 32 33 oveq123d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) )
35 3 oveqdr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r𝑅 ) 𝑧 ) )
36 27 29 35 oveq123d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) )
37 8 34 36 3eqtr3d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) )
38 31 37 jca ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵𝑧𝐵 ) ) → ( ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) ) )
39 22 38 syldan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) ) )
40 39 ralrimivvva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) ) )
41 eqid ( +g𝑅 ) = ( +g𝑅 )
42 10 9 41 13 isrng ( 𝑅 ∈ Rng ↔ ( 𝑅 ∈ Abel ∧ ( mulGrp ‘ 𝑅 ) ∈ Smgrp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r𝑅 ) 𝑦 ) ( +g𝑅 ) ( 𝑥 ( .r𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g𝑅 ) 𝑦 ) ( .r𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r𝑅 ) 𝑧 ) ( +g𝑅 ) ( 𝑦 ( .r𝑅 ) 𝑧 ) ) ) ) )
43 4 17 40 42 syl3anbrc ( 𝜑𝑅 ∈ Rng )