Theorem rngpropd 13913

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.)

Hypotheses

Ref	Expression
rngpropd.1	|- ( ph -> B = ( Base ` K ) )
rngpropd.2	|- ( ph -> B = ( Base ` L ) )
rngpropd.3	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
rngpropd.4	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )

Assertion

Ref	Expression
rngpropd	|- ( ph -> ( K e. Rng <-> L e. Rng ) )

Distinct variable groups:   x, y, B   x, K, y   ph, x, y   x, L, y

Proof of Theorem rngpropd

Dummy variables v u w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 527	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ph )
2		simprll 537	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. B )
3		simplrl 535	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. Abel )
4		simprlr 538	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. B )
5		rngpropd.1	. . . . . . . . . . . . . . . . 17 |- ( ph -> B = ( Base ` K ) )
6	5	ad2antrr 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> B = ( Base ` K ) )
7	4, 6	eleqtrd 2308	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` K ) )
8		simprr 531	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. B )
9	8, 6	eleqtrd 2308	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` K ) )
10		ablgrp 13821	. . . . . . . . . . . . . . . 16 |- ( K e. Abel -> K e. Grp )
11		eqid 2229	. . . . . . . . . . . . . . . . 17 |- ( Base ` K ) = ( Base ` K )
12		eqid 2229	. . . . . . . . . . . . . . . . 17 |- ( +g ` K ) = ( +g ` K )
13	11, 12	grpcl 13536	. . . . . . . . . . . . . . . 16 |- ( ( K e. Grp /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
14	10, 13	syl3an1 1304	. . . . . . . . . . . . . . 15 |- ( ( K e. Abel /\ v e. ( Base ` K ) /\ w e. ( Base ` K ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
15	3, 7, 9, 14	syl3anc 1271	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. ( Base ` K ) )
16	15, 6	eleqtrrd 2309	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) e. B )
17		rngpropd.4	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
18	17	oveqrspc2v 6027	. . . . . . . . . . . . 13 |- ( ( ph /\ ( u e. B /\ ( v ( +g ` K ) w ) e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
19	1, 2, 16, 18	syl12anc 1269	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` K ) w ) ) )
20		rngpropd.3	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
21	20	oveqrspc2v 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
22	1, 4, 8, 21	syl12anc 1269	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` K ) w ) = ( v ( +g ` L ) w ) )
23	22	oveq2d 6016	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` L ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
24	19, 23	eqtrd 2262	. . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( u ( .r ` L ) ( v ( +g ` L ) w ) ) )
25		simplrr 536	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> (mulGrp ` K ) e. Smgrp )
26	2, 6	eleqtrd 2308	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` K ) )
27	3	elexd 2813	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> K e. _V )
28		eqid 2229	. . . . . . . . . . . . . . . . . . 19 |- (mulGrp ` K ) = (mulGrp ` K )
29	28, 11	mgpbasg 13884	. . . . . . . . . . . . . . . . . 18 |- ( K e. _V -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
30	27, 29	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
31	26, 30	eleqtrd 2308	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> u e. ( Base ` (mulGrp ` K ) ) )
32	7, 30	eleqtrd 2308	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> v e. ( Base ` (mulGrp ` K ) ) )
33		eqid 2229	. . . . . . . . . . . . . . . . 17 |- ( Base ` (mulGrp ` K ) ) = ( Base ` (mulGrp ` K ) )
34		eqid 2229	. . . . . . . . . . . . . . . . 17 |- ( +g ` (mulGrp ` K ) ) = ( +g ` (mulGrp ` K ) )
35	33, 34	sgrpcl 13437	. . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ u e. ( Base ` (mulGrp ` K ) ) /\ v e. ( Base ` (mulGrp ` K ) ) ) -> ( u ( +g ` (mulGrp ` K ) ) v ) e. ( Base ` (mulGrp ` K ) ) )
36	25, 31, 32, 35	syl3anc 1271	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` (mulGrp ` K ) ) v ) e. ( Base ` (mulGrp ` K ) ) )
37		eqid 2229	. . . . . . . . . . . . . . . . . 18 |- ( .r ` K ) = ( .r ` K )
38	28, 37	mgpplusgg 13882	. . . . . . . . . . . . . . . . 17 |- ( K e. _V -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
39	27, 38	syl 14	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
40	39	oveqd 6017	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( +g ` (mulGrp ` K ) ) v ) )
41	36, 40, 30	3eltr4d 2313	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. ( Base ` K ) )
42	41, 6	eleqtrrd 2309	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) e. B )
43	9, 30	eleqtrd 2308	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> w e. ( Base ` (mulGrp ` K ) ) )
44	33, 34	sgrpcl 13437	. . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ u e. ( Base ` (mulGrp ` K ) ) /\ w e. ( Base ` (mulGrp ` K ) ) ) -> ( u ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
45	25, 31, 43, 44	syl3anc 1271	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
46	39	oveqd 6017	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( +g ` (mulGrp ` K ) ) w ) )
47	45, 46, 30	3eltr4d 2313	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. ( Base ` K ) )
48	47, 6	eleqtrrd 2309	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) e. B )
49	20	oveqrspc2v 6027	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( .r ` K ) v ) e. B /\ ( u ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
50	1, 42, 48, 49	syl12anc 1269	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) )
51	17	oveqrspc2v 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
52	51	ad2ant2r 509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) v ) = ( u ( .r ` L ) v ) )
53	17	oveqrspc2v 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
54	1, 2, 8, 53	syl12anc 1269	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( .r ` K ) w ) = ( u ( .r ` L ) w ) )
55	52, 54	oveq12d 6018	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` L ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
56	50, 55	eqtrd 2262	. . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) )
57	24, 56	eqeq12d 2244	. . . . . . . . . 10 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) <-> ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) ) )
58	11, 12	grpcl 13536	. . . . . . . . . . . . . . . 16 |- ( ( K e. Grp /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
59	10, 58	syl3an1 1304	. . . . . . . . . . . . . . 15 |- ( ( K e. Abel /\ u e. ( Base ` K ) /\ v e. ( Base ` K ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
60	3, 26, 7, 59	syl3anc 1271	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. ( Base ` K ) )
61	60, 6	eleqtrrd 2309	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) e. B )
62	17	oveqrspc2v 6027	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( +g ` K ) v ) e. B /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
63	1, 61, 8, 62	syl12anc 1269	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` K ) v ) ( .r ` L ) w ) )
64	20	oveqrspc2v 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
65	64	ad2ant2r 509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( u ( +g ` K ) v ) = ( u ( +g ` L ) v ) )
66	65	oveq1d 6015	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` L ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
67	63, 66	eqtrd 2262	. . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( +g ` L ) v ) ( .r ` L ) w ) )
68	33, 34	sgrpcl 13437	. . . . . . . . . . . . . . . 16 |- ( ( (mulGrp ` K ) e. Smgrp /\ v e. ( Base ` (mulGrp ` K ) ) /\ w e. ( Base ` (mulGrp ` K ) ) ) -> ( v ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
69	25, 32, 43, 68	syl3anc 1271	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( +g ` (mulGrp ` K ) ) w ) e. ( Base ` (mulGrp ` K ) ) )
70	39	oveqd 6017	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( +g ` (mulGrp ` K ) ) w ) )
71	69, 70, 30	3eltr4d 2313	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. ( Base ` K ) )
72	71, 6	eleqtrrd 2309	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) e. B )
73	20	oveqrspc2v 6027	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( u ( .r ` K ) w ) e. B /\ ( v ( .r ` K ) w ) e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
74	1, 48, 72, 73	syl12anc 1269	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) )
75	17	oveqrspc2v 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( v e. B /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
76	1, 4, 8, 75	syl12anc 1269	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( v ( .r ` K ) w ) = ( v ( .r ` L ) w ) )
77	54, 76	oveq12d 6018	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` L ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
78	74, 77	eqtrd 2262	. . . . . . . . . . 11 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) )
79	67, 78	eqeq12d 2244	. . . . . . . . . 10 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) <-> ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) )
80	57, 79	anbi12d 473	. . . . . . . . 9 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( ( u e. B /\ v e. B ) /\ w e. B ) ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
81	80	anassrs 400	. . . . . . . 8 |- ( ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) /\ w e. B ) -> ( ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
82	81	ralbidva 2526	. . . . . . 7 |- ( ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) /\ ( u e. B /\ v e. B ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
83	82	2ralbidva 2552	. . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
84	5	adantr 276	. . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` K ) )
85	84	raleqdv 2734	. . . . . . . 8 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
86	84, 85	raleqbidv 2744	. . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
87	84, 86	raleqbidv 2744	. . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
88		rngpropd.2	. . . . . . . 8 |- ( ph -> B = ( Base ` L ) )
89	88	adantr 276	. . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> B = ( Base ` L ) )
90	89	raleqdv 2734	. . . . . . . 8 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
91	89, 90	raleqbidv 2744	. . . . . . 7 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
92	89, 91	raleqbidv 2744	. . . . . 6 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. B A. v e. B A. w e. B ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
93	83, 87, 92	3bitr3d 218	. . . . 5 |- ( ( ph /\ ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) ) -> ( A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) <-> A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
94	93	pm5.32da 452	. . . 4 |- ( ph -> ( ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
95		df-3an 1004	. . . 4 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
96		df-3an 1004	. . . 4 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp ) /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
97	94, 95, 96	3bitr4g 223	. . 3 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
98		simp1 1021	. . . . 5 |- ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel )
99	98	a1i 9	. . . 4 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel ) )
100		simp1 1021	. . . . 5 |- ( ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> L e. Abel )
101	5, 88, 20	ablpropd 13828	. . . . 5 |- ( ph -> ( K e. Abel <-> L e. Abel ) )
102	100, 101	imbitrrid 156	. . . 4 |- ( ph -> ( ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) -> K e. Abel ) )
103	101	adantr 276	. . . . . 6 |- ( ( ph /\ K e. Abel ) -> ( K e. Abel <-> L e. Abel ) )
104	28	mgpex 13883	. . . . . . . 8 |- ( K e. Abel -> (mulGrp ` K ) e. _V )
105	104	adantl 277	. . . . . . 7 |- ( ( ph /\ K e. Abel ) -> (mulGrp ` K ) e. _V )
106	101	biimpa 296	. . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> L e. Abel )
107		eqid 2229	. . . . . . . . 9 |- (mulGrp ` L ) = (mulGrp ` L )
108	107	mgpex 13883	. . . . . . . 8 |- ( L e. Abel -> (mulGrp ` L ) e. _V )
109	106, 108	syl 14	. . . . . . 7 |- ( ( ph /\ K e. Abel ) -> (mulGrp ` L ) e. _V )
110		elex 2811	. . . . . . . . 9 |- ( K e. Abel -> K e. _V )
111	110	adantl 277	. . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> K e. _V )
112	111, 29	syl 14	. . . . . . 7 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = ( Base ` (mulGrp ` K ) ) )
113	5	eqcomd 2235	. . . . . . . . 9 |- ( ph -> ( Base ` K ) = B )
114	113	adantr 276	. . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = B )
115	88	adantr 276	. . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> B = ( Base ` L ) )
116		eqid 2229	. . . . . . . . . . 11 |- ( Base ` L ) = ( Base ` L )
117	107, 116	mgpbasg 13884	. . . . . . . . . 10 |- ( L e. Abel -> ( Base ` L ) = ( Base ` (mulGrp ` L ) ) )
118	106, 117	syl 14	. . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( Base ` L ) = ( Base ` (mulGrp ` L ) ) )
119	115, 118	eqtrd 2262	. . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> B = ( Base ` (mulGrp ` L ) ) )
120	114, 119	eqtrd 2262	. . . . . . 7 |- ( ( ph /\ K e. Abel ) -> ( Base ` K ) = ( Base ` (mulGrp ` L ) ) )
121	17	ex 115	. . . . . . . . . 10 |- ( ph -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
122	121	adantr 276	. . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x e. B /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
123	5	eleq2d 2299	. . . . . . . . . . . 12 |- ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
124	5	eleq2d 2299	. . . . . . . . . . . 12 |- ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
125	123, 124	anbi12d 473	. . . . . . . . . . 11 |- ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) )
126	125	bicomd 141	. . . . . . . . . 10 |- ( ph -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> ( x e. B /\ y e. B ) ) )
127	126	adantr 276	. . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> ( x e. B /\ y e. B ) ) )
128	111, 38	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ K e. Abel ) -> ( .r ` K ) = ( +g ` (mulGrp ` K ) ) )
129	128	eqcomd 2235	. . . . . . . . . . 11 |- ( ( ph /\ K e. Abel ) -> ( +g ` (mulGrp ` K ) ) = ( .r ` K ) )
130	129	oveqd 6017	. . . . . . . . . 10 |- ( ( ph /\ K e. Abel ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( .r ` K ) y ) )
131		eqid 2229	. . . . . . . . . . . . . 14 |- ( .r ` L ) = ( .r ` L )
132	107, 131	mgpplusgg 13882	. . . . . . . . . . . . 13 |- ( L e. Abel -> ( .r ` L ) = ( +g ` (mulGrp ` L ) ) )
133	106, 132	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ K e. Abel ) -> ( .r ` L ) = ( +g ` (mulGrp ` L ) ) )
134	133	eqcomd 2235	. . . . . . . . . . 11 |- ( ( ph /\ K e. Abel ) -> ( +g ` (mulGrp ` L ) ) = ( .r ` L ) )
135	134	oveqd 6017	. . . . . . . . . 10 |- ( ( ph /\ K e. Abel ) -> ( x ( +g ` (mulGrp ` L ) ) y ) = ( x ( .r ` L ) y ) )
136	130, 135	eqeq12d 2244	. . . . . . . . 9 |- ( ( ph /\ K e. Abel ) -> ( ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) <-> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) ) )
137	122, 127, 136	3imtr4d 203	. . . . . . . 8 |- ( ( ph /\ K e. Abel ) -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) ) )
138	137	imp 124	. . . . . . 7 |- ( ( ( ph /\ K e. Abel ) /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` (mulGrp ` K ) ) y ) = ( x ( +g ` (mulGrp ` L ) ) y ) )
139	105, 109, 112, 120, 138	sgrppropd 13441	. . . . . 6 |- ( ( ph /\ K e. Abel ) -> ( (mulGrp ` K ) e. Smgrp <-> (mulGrp ` L ) e. Smgrp ) )
140	103, 139	3anbi12d 1347	. . . . 5 |- ( ( ph /\ K e. Abel ) -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
141	140	ex 115	. . . 4 |- ( ph -> ( K e. Abel -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) ) )
142	99, 102, 141	pm5.21ndd 710	. . 3 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
143	97, 142	bitrd 188	. 2 |- ( ph -> ( ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) ) )
144	11, 28, 12, 37	isrng 13892	. 2 |- ( K e. Rng <-> ( K e. Abel /\ (mulGrp ` K ) e. Smgrp /\ A. u e. ( Base ` K ) A. v e. ( Base ` K ) A. w e. ( Base ` K ) ( ( u ( .r ` K ) ( v ( +g ` K ) w ) ) = ( ( u ( .r ` K ) v ) ( +g ` K ) ( u ( .r ` K ) w ) ) /\ ( ( u ( +g ` K ) v ) ( .r ` K ) w ) = ( ( u ( .r ` K ) w ) ( +g ` K ) ( v ( .r ` K ) w ) ) ) ) )
145		eqid 2229	. . 3 |- ( +g ` L ) = ( +g ` L )
146	116, 107, 145, 131	isrng 13892	. 2 |- ( L e. Rng <-> ( L e. Abel /\ (mulGrp ` L ) e. Smgrp /\ A. u e. ( Base ` L ) A. v e. ( Base ` L ) A. w e. ( Base ` L ) ( ( u ( .r ` L ) ( v ( +g ` L ) w ) ) = ( ( u ( .r ` L ) v ) ( +g ` L ) ( u ( .r ` L ) w ) ) /\ ( ( u ( +g ` L ) v ) ( .r ` L ) w ) = ( ( u ( .r ` L ) w ) ( +g ` L ) ( v ( .r ` L ) w ) ) ) ) )
147	143, 144, 146	3bitr4g 223	1 |- ( ph -> ( K e. Rng <-> L e. Rng ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1002   = wceq 1395   e. wcel 2200   A.wral 2508   _Vcvv 2799   ` cfv 5317  (class class class)co 6000   Basecbs 13027   +g cplusg 13105   .rcmulr 13106  Smgrpcsgrp 13429   Grpcgrp 13528   Abelcabl 13817  mulGrpcmgp 13878  Rngcrng 13890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-i2m1 8100  ax-0lt1 8101  ax-0id 8103  ax-rnegex 8104  ax-pre-ltirr 8107  ax-pre-ltadd 8111

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-iota 5277  df-fun 5319  df-fn 5320  df-fv 5325  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-pnf 8179  df-mnf 8180  df-ltxr 8182  df-inn 9107  df-2 9165  df-3 9166  df-ndx 13030  df-slot 13031  df-base 13033  df-sets 13034  df-plusg 13118  df-mulr 13119  df-0g 13286  df-mgm 13384  df-sgrp 13430  df-mnd 13445  df-grp 13531  df-cmn 13818  df-abl 13819  df-mgp 13879  df-rng 13891

This theorem is referenced by:  opprrngbg  14036  subrngpropd  14174