Metamath Proof Explorer


Theorem rngpropd

Description: If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypotheses rngpropd.1 φB=BaseK
rngpropd.2 φB=BaseL
rngpropd.3 φxByBx+Ky=x+Ly
rngpropd.4 φxByBxKy=xLy
Assertion rngpropd φKRngLRng

Proof

Step Hyp Ref Expression
1 rngpropd.1 φB=BaseK
2 rngpropd.2 φB=BaseL
3 rngpropd.3 φxByBx+Ky=x+Ly
4 rngpropd.4 φxByBxKy=xLy
5 simpll φKAbelmulGrpKSmgrpuBvBwBφ
6 simprll φKAbelmulGrpKSmgrpuBvBwBuB
7 simplrl φKAbelmulGrpKSmgrpuBvBwBKAbel
8 simprlr φKAbelmulGrpKSmgrpuBvBwBvB
9 1 ad2antrr φKAbelmulGrpKSmgrpuBvBwBB=BaseK
10 8 9 eleqtrd φKAbelmulGrpKSmgrpuBvBwBvBaseK
11 simprr φKAbelmulGrpKSmgrpuBvBwBwB
12 11 9 eleqtrd φKAbelmulGrpKSmgrpuBvBwBwBaseK
13 ablgrp KAbelKGrp
14 eqid BaseK=BaseK
15 eqid +K=+K
16 14 15 grpcl KGrpvBaseKwBaseKv+KwBaseK
17 13 16 syl3an1 KAbelvBaseKwBaseKv+KwBaseK
18 7 10 12 17 syl3anc φKAbelmulGrpKSmgrpuBvBwBv+KwBaseK
19 18 9 eleqtrrd φKAbelmulGrpKSmgrpuBvBwBv+KwB
20 4 oveqrspc2v φuBv+KwBuKv+Kw=uLv+Kw
21 5 6 19 20 syl12anc φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uLv+Kw
22 3 oveqrspc2v φvBwBv+Kw=v+Lw
23 5 8 11 22 syl12anc φKAbelmulGrpKSmgrpuBvBwBv+Kw=v+Lw
24 23 oveq2d φKAbelmulGrpKSmgrpuBvBwBuLv+Kw=uLv+Lw
25 21 24 eqtrd φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uLv+Lw
26 simplrr φKAbelmulGrpKSmgrpuBvBwBmulGrpKSmgrp
27 6 9 eleqtrd φKAbelmulGrpKSmgrpuBvBwBuBaseK
28 eqid mulGrpK=mulGrpK
29 28 14 mgpbas BaseK=BasemulGrpK
30 eqid K=K
31 28 30 mgpplusg K=+mulGrpK
32 29 31 sgrpcl mulGrpKSmgrpuBaseKvBaseKuKvBaseK
33 26 27 10 32 syl3anc φKAbelmulGrpKSmgrpuBvBwBuKvBaseK
34 33 9 eleqtrrd φKAbelmulGrpKSmgrpuBvBwBuKvB
35 29 31 sgrpcl mulGrpKSmgrpuBaseKwBaseKuKwBaseK
36 26 27 12 35 syl3anc φKAbelmulGrpKSmgrpuBvBwBuKwBaseK
37 36 9 eleqtrrd φKAbelmulGrpKSmgrpuBvBwBuKwB
38 3 oveqrspc2v φuKvBuKwBuKv+KuKw=uKv+LuKw
39 5 34 37 38 syl12anc φKAbelmulGrpKSmgrpuBvBwBuKv+KuKw=uKv+LuKw
40 4 oveqrspc2v φuBvBuKv=uLv
41 40 ad2ant2r φKAbelmulGrpKSmgrpuBvBwBuKv=uLv
42 4 oveqrspc2v φuBwBuKw=uLw
43 5 6 11 42 syl12anc φKAbelmulGrpKSmgrpuBvBwBuKw=uLw
44 41 43 oveq12d φKAbelmulGrpKSmgrpuBvBwBuKv+LuKw=uLv+LuLw
45 39 44 eqtrd φKAbelmulGrpKSmgrpuBvBwBuKv+KuKw=uLv+LuLw
46 25 45 eqeq12d φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwuLv+Lw=uLv+LuLw
47 14 15 grpcl KGrpuBaseKvBaseKu+KvBaseK
48 13 47 syl3an1 KAbeluBaseKvBaseKu+KvBaseK
49 7 27 10 48 syl3anc φKAbelmulGrpKSmgrpuBvBwBu+KvBaseK
50 49 9 eleqtrrd φKAbelmulGrpKSmgrpuBvBwBu+KvB
51 4 oveqrspc2v φu+KvBwBu+KvKw=u+KvLw
52 5 50 11 51 syl12anc φKAbelmulGrpKSmgrpuBvBwBu+KvKw=u+KvLw
53 3 oveqrspc2v φuBvBu+Kv=u+Lv
54 53 ad2ant2r φKAbelmulGrpKSmgrpuBvBwBu+Kv=u+Lv
55 54 oveq1d φKAbelmulGrpKSmgrpuBvBwBu+KvLw=u+LvLw
56 52 55 eqtrd φKAbelmulGrpKSmgrpuBvBwBu+KvKw=u+LvLw
57 29 31 sgrpcl mulGrpKSmgrpvBaseKwBaseKvKwBaseK
58 26 10 12 57 syl3anc φKAbelmulGrpKSmgrpuBvBwBvKwBaseK
59 58 9 eleqtrrd φKAbelmulGrpKSmgrpuBvBwBvKwB
60 3 oveqrspc2v φuKwBvKwBuKw+KvKw=uKw+LvKw
61 5 37 59 60 syl12anc φKAbelmulGrpKSmgrpuBvBwBuKw+KvKw=uKw+LvKw
62 4 oveqrspc2v φvBwBvKw=vLw
63 5 8 11 62 syl12anc φKAbelmulGrpKSmgrpuBvBwBvKw=vLw
64 43 63 oveq12d φKAbelmulGrpKSmgrpuBvBwBuKw+LvKw=uLw+LvLw
65 61 64 eqtrd φKAbelmulGrpKSmgrpuBvBwBuKw+KvKw=uLw+LvLw
66 56 65 eqeq12d φKAbelmulGrpKSmgrpuBvBwBu+KvKw=uKw+KvKwu+LvLw=uLw+LvLw
67 46 66 anbi12d φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
68 67 anassrs φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
69 68 ralbidva φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwwBuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
70 69 2ralbidva φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwuBvBwBuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
71 1 adantr φKAbelmulGrpKSmgrpB=BaseK
72 71 raleqdv φKAbelmulGrpKSmgrpwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKw
73 71 72 raleqbidv φKAbelmulGrpKSmgrpvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKw
74 71 73 raleqbidv φKAbelmulGrpKSmgrpuBvBwBuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKw
75 2 adantr φKAbelmulGrpKSmgrpB=BaseL
76 75 raleqdv φKAbelmulGrpKSmgrpwBuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLwwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
77 75 76 raleqbidv φKAbelmulGrpKSmgrpvBwBuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLwvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
78 75 77 raleqbidv φKAbelmulGrpKSmgrpuBvBwBuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLwuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
79 70 74 78 3bitr3d φKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
80 79 pm5.32da φKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwKAbelmulGrpKSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
81 df-3an KAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKw
82 df-3an KAbelmulGrpKSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLwKAbelmulGrpKSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
83 80 81 82 3bitr4g φKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwKAbelmulGrpKSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
84 1 2 3 ablpropd φKAbelLAbel
85 fvexd φmulGrpKV
86 fvexd φmulGrpLV
87 29 a1i φBaseK=BasemulGrpK
88 eqid mulGrpL=mulGrpL
89 eqid BaseL=BaseL
90 88 89 mgpbas BaseL=BasemulGrpL
91 2 90 eqtrdi φB=BasemulGrpL
92 1 91 eqtr3d φBaseK=BasemulGrpL
93 4 ex φxByBxKy=xLy
94 1 eleq2d φxBxBaseK
95 1 eleq2d φyByBaseK
96 94 95 anbi12d φxByBxBaseKyBaseK
97 96 bicomd φxBaseKyBaseKxByB
98 31 a1i φK=+mulGrpK
99 98 eqcomd φ+mulGrpK=K
100 99 oveqd φx+mulGrpKy=xKy
101 eqid L=L
102 88 101 mgpplusg L=+mulGrpL
103 102 a1i φL=+mulGrpL
104 103 eqcomd φ+mulGrpL=L
105 104 oveqd φx+mulGrpLy=xLy
106 100 105 eqeq12d φx+mulGrpKy=x+mulGrpLyxKy=xLy
107 93 97 106 3imtr4d φxBaseKyBaseKx+mulGrpKy=x+mulGrpLy
108 107 imp φxBaseKyBaseKx+mulGrpKy=x+mulGrpLy
109 85 86 87 92 108 sgrppropd φmulGrpKSmgrpmulGrpLSmgrp
110 84 109 3anbi12d φKAbelmulGrpKSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLwLAbelmulGrpLSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
111 83 110 bitrd φKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKwLAbelmulGrpLSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
112 14 28 15 30 isrng KRngKAbelmulGrpKSmgrpuBaseKvBaseKwBaseKuKv+Kw=uKv+KuKwu+KvKw=uKw+KvKw
113 eqid +L=+L
114 89 88 113 101 isrng LRngLAbelmulGrpLSmgrpuBaseLvBaseLwBaseLuLv+Lw=uLv+LuLwu+LvLw=uLw+LvLw
115 111 112 114 3bitr4g φKRngLRng