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 20144

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 19749	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Abel → 𝐾 ∈ Grp)
11		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
13	11, 12	grpcl 18906	. . . . . . . . . . . . . . . 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 7385	. . . . . . . . . . . . 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 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
22	1, 4, 8, 21	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
23	22	oveq2d 7374	. . . . . . . . . . . 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 20115	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
29		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝐾) = (._r‘𝐾)
30	27, 29	mgpplusg 20114	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝐾) = (+_g‘(mulGrp‘𝐾))
31	28, 30	sgrpcl 18683	. . . . . . . . . . . . . . 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 18683	. . . . . . . . . . . . . . 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 7385	. . . . . . . . . . . . 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 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
40	39	ad2ant2r 748	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
41	17	oveqrspc2v 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
42	1, 2, 8, 41	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
43	40, 42	oveq12d 7376	. . . . . . . . . . . 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 18906	. . . . . . . . . . . . . . . 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 7385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(+_g‘𝐾)𝑣) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
51	1, 49, 8, 50	syl12anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
52	20	oveqrspc2v 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
53	52	ad2ant2r 748	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
54	53	oveq1d 7373	. . . . . . . . . . . 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 18683	. . . . . . . . . . . . . . 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 7385	. . . . . . . . . . . . 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 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
62	1, 4, 8, 61	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
63	42, 62	oveq12d 7376	. . . . . . . . . . . 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 3296	. . . . . . . 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 3312	. . . . . . 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 3312	. . . . . 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 3296	. . . . . . . 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 3312	. . . . . . 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 3312	. . . . . 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 19756	. . . 4 ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
85		fvexd 6847	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ V)
86		fvexd 6847	. . . . 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 20115	. . . . . . 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 7375	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(._r‘𝐾)𝑦))
101		eqid 2737	. . . . . . . . . . . 12 ⊢ (._r‘𝐿) = (._r‘𝐿)
102	88, 101	mgpplusg 20114	. . . . . . . . . . 11 ⊢ (._r‘𝐿) = (+_g‘(mulGrp‘𝐿))
103	102	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐿) = (+_g‘(mulGrp‘𝐿)))
104	103	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐿)) = (._r‘𝐿))
105	104	oveqd 7375	. . . . . . . 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 18688	. . . 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 20124	. 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 20124	. 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 3430 ‘cfv 6490 (class class class)co 7358 Basecbs 17168 +_gcplusg 17209 ._rcmulr 17210 Smgrpcsgrp 18675 Grpcgrp 18898 Abelcabl 19745 mulGrpcmgp 20110 Rngcrng 20122

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 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

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 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-2nd 7934 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12164 df-2 12233 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-plusg 17222 df-0g 17393 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-grp 18901 df-cmn 19746 df-abl 19747 df-mgp 20111 df-rng 20123

This theorem is referenced by: opprrngb 20315 subrngpropd 20534

W3C validator