rngpropd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rngpropd		Structured version Visualization version GIF version

Theorem rngpropd 20121

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	⊢ (𝜑 → 𝐵 = (Base‘𝐾))
rngpropd.2	⊢ (𝜑 → 𝐵 = (Base‘𝐿))
rngpropd.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
rngpropd.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦))

**Assertion**
Ref	Expression
rngpropd	⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng))

Distinct variable groups: 𝑥,𝑦,𝐵 𝑥,𝐾,𝑦 𝜑,𝑥,𝑦 𝑥,𝐿,𝑦

Proof of Theorem rngpropd Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝜑)
2		simprll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ 𝐵)
3		simplrl 777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐾 ∈ Abel)
4		simprlr 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ 𝐵)
5		rngpropd.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
6	5	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐵 = (Base‘𝐾))
7	4, 6	eleqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ (Base‘𝐾))
8		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
9	8, 6	eleqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ (Base‘𝐾))
10		ablgrp 19726	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Abel → 𝐾 ∈ Grp)
11		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
13	11, 12	grpcl 18883	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
14	10, 13	syl3an1 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
15	3, 7, 9, 14	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
16	15, 6	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)
17		rngpropd.4	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦))
18	17	oveqrspc2v 7395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
19	1, 2, 16, 18	syl12anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
20		rngpropd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
21	20	oveqrspc2v 7395	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
22	1, 4, 8, 21	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
23	22	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
24	19, 23	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
25		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (mulGrp‘𝐾) ∈ Smgrp)
26	2, 6	eleqtrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ (Base‘𝐾))
27		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
28	27, 11	mgpbas 20092	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
29		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝐾) = (._r‘𝐾)
30	27, 29	mgpplusg 20091	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝐾) = (+_g‘(mulGrp‘𝐾))
31	28, 30	sgrpcl 18663	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
32	25, 26, 7, 31	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
33	32, 6	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ 𝐵)
34	28, 30	sgrpcl 18663	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
35	25, 26, 9, 34	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
36	35, 6	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)
37	20	oveqrspc2v 7395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑣) ∈ 𝐵 ∧ (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
38	1, 33, 36, 37	syl12anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
39	17	oveqrspc2v 7395	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
40	39	ad2ant2r 748	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
41	17	oveqrspc2v 7395	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
42	1, 2, 8, 41	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
43	40, 42	oveq12d 7386	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
44	38, 43	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
45	24, 44	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ↔ (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤))))
46	11, 12	grpcl 18883	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
47	10, 46	syl3an1 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
48	3, 26, 7, 47	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
49	48, 6	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ 𝐵)
50	17	oveqrspc2v 7395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(+_g‘𝐾)𝑣) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
51	1, 49, 8, 50	syl12anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
52	20	oveqrspc2v 7395	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
53	52	ad2ant2r 748	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
54	53	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
55	51, 54	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
56	28, 30	sgrpcl 18663	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
57	25, 7, 9, 56	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
58	57, 6	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)
59	20	oveqrspc2v 7395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
60	1, 36, 58, 59	syl12anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
61	17	oveqrspc2v 7395	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
62	1, 4, 8, 61	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
63	42, 62	oveq12d 7386	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
64	60, 63	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
65	55, 64	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) ↔ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))
66	45, 65	anbi12d 633	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
67	66	anassrs 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ 𝑤 ∈ 𝐵) → (((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
68	67	ralbidva 3159	. . . . . . 7 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
69	68	2ralbidva 3200	. . . . . 6 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
70	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐾))
71	70	raleqdv 3298	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
72	70, 71	raleqbidv 3318	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
73	70, 72	raleqbidv 3318	. . . . . 6 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
74		rngpropd.2	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (Base‘𝐿))
75	74	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐿))
76	75	raleqdv 3298	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))) ↔ ∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
77	75, 76	raleqbidv 3318	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))) ↔ ∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
78	75, 77	raleqbidv 3318	. . . . . 6 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
79	69, 73, 78	3bitr3d 309	. . . . 5 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → (∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤))) ↔ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
80	79	pm5.32da 579	. . . 4 ⊢ (𝜑 → (((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp) ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))) ↔ ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp) ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))))
81		df-3an 1089	. . . 4 ⊢ ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))) ↔ ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp) ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
82		df-3an 1089	. . . 4 ⊢ ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))) ↔ ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp) ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
83	80, 81, 82	3bitr4g 314	. . 3 ⊢ (𝜑 → ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))) ↔ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))))
84	5, 74, 20	ablpropd 19733	. . . 4 ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
85		fvexd 6857	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ V)
86		fvexd 6857	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐿) ∈ V)
87	28	a1i 11	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
88		eqid 2737	. . . . . . . 8 ⊢ (mulGrp‘𝐿) = (mulGrp‘𝐿)
89		eqid 2737	. . . . . . . 8 ⊢ (Base‘𝐿) = (Base‘𝐿)
90	88, 89	mgpbas 20092	. . . . . . 7 ⊢ (Base‘𝐿) = (Base‘(mulGrp‘𝐿))
91	74, 90	eqtrdi 2788	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘(mulGrp‘𝐿)))
92	5, 91	eqtr3d 2774	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐿)))
93	17	ex 412	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
94	5	eleq2d 2823	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾)))
95	5	eleq2d 2823	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐾)))
96	94, 95	anbi12d 633	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))))
97	96	bicomd 223	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
98	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐾) = (+_g‘(mulGrp‘𝐾)))
99	98	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾))
100	99	oveqd 7385	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(._r‘𝐾)𝑦))
101		eqid 2737	. . . . . . . . . . . 12 ⊢ (._r‘𝐿) = (._r‘𝐿)
102	88, 101	mgpplusg 20091	. . . . . . . . . . 11 ⊢ (._r‘𝐿) = (+_g‘(mulGrp‘𝐿))
103	102	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐿) = (+_g‘(mulGrp‘𝐿)))
104	103	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐿)) = (._r‘𝐿))
105	104	oveqd 7385	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐿))𝑦) = (𝑥(._r‘𝐿)𝑦))
106	100, 105	eqeq12d 2753	. . . . . . 7 ⊢ (𝜑 → ((𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦) ↔ (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
107	93, 97, 106	3imtr4d 294	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦)))
108	107	imp 406	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
109	85, 86, 87, 92, 108	sgrppropd 18668	. . . 4 ⊢ (𝜑 → ((mulGrp‘𝐾) ∈ Smgrp ↔ (mulGrp‘𝐿) ∈ Smgrp))
110	84, 109	3anbi12d 1440	. . 3 ⊢ (𝜑 → ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))) ↔ (𝐿 ∈ Abel ∧ (mulGrp‘𝐿) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))))
111	83, 110	bitrd 279	. 2 ⊢ (𝜑 → ((𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))) ↔ (𝐿 ∈ Abel ∧ (mulGrp‘𝐿) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))))
112	11, 27, 12, 29	isrng 20101	. 2 ⊢ (𝐾 ∈ Rng ↔ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
113		eqid 2737	. . 3 ⊢ (+_g‘𝐿) = (+_g‘𝐿)
114	89, 88, 113, 101	isrng 20101	. 2 ⊢ (𝐿 ∈ Rng ↔ (𝐿 ∈ Abel ∧ (mulGrp‘𝐿) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
115	111, 112, 114	3bitr4g 314	1 ⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3442 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 +_gcplusg 17189 ._rcmulr 17190 Smgrpcsgrp 18655 Grpcgrp 18875 Abelcabl 19722 mulGrpcmgp 20087 Rngcrng 20099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-plusg 17202 df-0g 17373 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-grp 18878 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100

This theorem is referenced by: opprrngb 20294 subrngpropd 20513

W3C validator