Metamath Proof Explorer

Theorem cznrng

Description: The ring constructed from a Z/nZ structure by replacing the (multiplicative) ring operation by a constant operation is a non-unital ring. (Contributed by AV, 17-Feb-2020)

Ref Expression
Hypotheses cznrng.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
cznrng.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
cznrng.x ⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
cznrng.0 ⊢ 0 = ( 0g ‘ 𝑌 )
Assertion cznrng ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng )

Proof

Step Hyp Ref Expression
1 cznrng.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 cznrng.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 cznrng.x ⊢ 𝑋 = ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ )
4 cznrng.0 ⊢ 0 = ( 0g ‘ 𝑌 )
5 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
6 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
7 5 6 syl ⊢ ( 𝑁 ∈ ℕ → 𝑌 ∈ CRing )
8 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
9 2 4 ring0cl ⊢ ( 𝑌 ∈ Ring → 0 ∈ 𝐵 )
10 eleq1a ⊢ ( 0 ∈ 𝐵 → ( 𝐶 = 0 → 𝐶 ∈ 𝐵 ) )
11 9 10 syl ⊢ ( 𝑌 ∈ Ring → ( 𝐶 = 0 → 𝐶 ∈ 𝐵 ) )
12 8 11 syl ⊢ ( 𝑌 ∈ CRing → ( 𝐶 = 0 → 𝐶 ∈ 𝐵 ) )
13 7 12 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝐶 = 0 → 𝐶 ∈ 𝐵 ) )
14 13 imp ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝐶 ∈ 𝐵 )
15 1 2 3 cznabel ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∈ Abel )
16 15 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → 𝑋 ∈ Abel )
17 eqid ⊢ ( mulGrp ‘ 𝑋 ) = ( mulGrp ‘ 𝑋 )
18 1 2 3 cznrnglem ⊢ 𝐵 = ( Base ‘ 𝑋 )
19 17 18 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑋 ) )
20 3 fveq2i ⊢ ( mulGrp ‘ 𝑋 ) = ( mulGrp ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
21 1 fvexi ⊢ 𝑌 ∈ V
22 2 fvexi ⊢ 𝐵 ∈ V
23 22 22 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V
24 mulridx ⊢ .r = Slot ( .r ‘ ndx )
25 24 setsid ⊢ ( ( 𝑌 ∈ V ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( .r ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) ) )
26 21 23 25 mp2an ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( .r ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
27 20 26 mgpplusg ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( +g ‘ ( mulGrp ‘ 𝑋 ) )
28 27 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑋 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
29 ne0i ⊢ ( 𝐶 ∈ 𝐵 → 𝐵 ≠ ∅ )
30 29 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 ≠ ∅ )
31 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
32 19 28 30 31 copissgrp ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → ( mulGrp ‘ 𝑋 ) ∈ Smgrp )
33 oveq1 ⊢ ( 𝐶 = 0 → ( 𝐶 ( +g ‘ 𝑌 ) 𝐶 ) = ( 0 ( +g ‘ 𝑌 ) 𝐶 ) )
34 33 ad3antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐶 ( +g ‘ 𝑌 ) 𝐶 ) = ( 0 ( +g ‘ 𝑌 ) 𝐶 ) )
35 7 8 syl ⊢ ( 𝑁 ∈ ℕ → 𝑌 ∈ Ring )
36 ringmnd ⊢ ( 𝑌 ∈ Ring → 𝑌 ∈ Mnd )
37 35 36 syl ⊢ ( 𝑁 ∈ ℕ → 𝑌 ∈ Mnd )
38 37 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑌 ∈ Mnd )
39 38 anim1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵 ) )
40 39 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵 ) )
41 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
42 2 41 4 mndlid ⊢ ( ( 𝑌 ∈ Mnd ∧ 𝐶 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑌 ) 𝐶 ) = 𝐶 )
43 40 42 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 0 ( +g ‘ 𝑌 ) 𝐶 ) = 𝐶 )
44 34 43 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝐶 ( +g ‘ 𝑌 ) 𝐶 ) = 𝐶 )
45 eqidd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
46 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → 𝐶 = 𝐶 )
47 simpr1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
48 simpr2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
49 31 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
50 45 46 47 48 49 ovmpod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) = 𝐶 )
51 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
52 simpr3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐵 )
53 45 51 47 52 49 ovmpod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
54 50 53 oveq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) = ( 𝐶 ( +g ‘ 𝑌 ) 𝐶 ) )
55 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) ) → 𝐶 = 𝐶 )
56 35 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑌 ∈ Ring )
57 2 41 ringacl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ 𝐵 )
58 56 48 52 57 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ 𝐵 )
59 45 55 47 58 49 ovmpod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = 𝐶 )
60 44 54 59 3eqtr4rd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) )
61 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑏 ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
62 45 61 48 52 49 ovmpod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
63 53 62 oveq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) = ( 𝐶 ( +g ‘ 𝑌 ) 𝐶 ) )
64 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑥 = ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∧ 𝑦 = 𝑐 ) ) → 𝐶 = 𝐶 )
65 2 41 ringacl ⊢ ( ( 𝑌 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
66 56 47 48 65 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ∈ 𝐵 )
67 45 64 66 52 49 ovmpod ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = 𝐶 )
68 44 63 67 3eqtr4rd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) )
69 60 68 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) )
70 69 ralrimivvva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) )
71 16 32 70 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝑋 ∈ Abel ∧ ( mulGrp ‘ 𝑋 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) ) )
72 14 71 mpdan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → ( 𝑋 ∈ Abel ∧ ( mulGrp ‘ 𝑋 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) ) )
73 plusgid ⊢ +g = Slot ( +g ‘ ndx )
74 plusgndxnmulrndx ⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
75 73 74 setsnid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
76 3 fveq2i ⊢ ( +g ‘ 𝑋 ) = ( +g ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) )
77 75 76 eqtr4i ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑋 )
78 3 eqcomi ⊢ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) = 𝑋
79 78 fveq2i ⊢ ( .r ‘ ( 𝑌 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ⟩ ) ) = ( .r ‘ 𝑋 )
80 26 79 eqtri ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( .r ‘ 𝑋 )
81 18 17 77 80 isrng ⊢ ( 𝑋 ∈ Rng ↔ ( 𝑋 ∈ Abel ∧ ( mulGrp ‘ 𝑋 ) ∈ Smgrp ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) = ( ( 𝑎 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) 𝑐 ) ) ) ) )
82 72 81 sylibr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐶 = 0 ) → 𝑋 ∈ Rng )