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 20243

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 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝜑)
2		simprll 790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ 𝐵)
3		simplrl 788	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐾 ∈ Abel)
4		simprlr 791	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ 𝐵)
5		rngpropd.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
6	5	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐵 = (Base‘𝐾))
7	4, 6	eleqtrd 2867	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ (Base‘𝐾))
8		simprr 784	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
9	8, 6	eleqtrd 2867	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ (Base‘𝐾))
10		ablgrp 19846	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Abel → 𝐾 ∈ Grp)
11		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
13	11, 12	grpcl 18998	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
14	10, 13	syl3an1 1179	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
15	3, 7, 9, 14	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
16	15, 6	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)
17		rngpropd.4	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦))
18	17	oveqrspc2v 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
19	1, 2, 16, 18	syl12anc 849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
20		rngpropd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
21	20	oveqrspc2v 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
22	1, 4, 8, 21	syl12anc 849	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
23	22	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
24	19, 23	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
25		simplrr 789	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (mulGrp‘𝐾) ∈ Smgrp)
26	2, 6	eleqtrd 2867	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ (Base‘𝐾))
27		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
28	27, 11	mgpbas 20212	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
29		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝐾) = (._r‘𝐾)
30	27, 29	mgpplusg 20211	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝐾) = (+_g‘(mulGrp‘𝐾))
31	28, 30	sgrpcl 18774	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
32	25, 26, 7, 31	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
33	32, 6	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ 𝐵)
34	28, 30	sgrpcl 18774	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
35	25, 26, 9, 34	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
36	35, 6	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)
37	20	oveqrspc2v 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑣) ∈ 𝐵 ∧ (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
38	1, 33, 36, 37	syl12anc 849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
39	17	oveqrspc2v 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
40	39	ad2ant2r 759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
41	17	oveqrspc2v 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
42	1, 2, 8, 41	syl12anc 849	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
43	40, 42	oveq12d 7418	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
44	38, 43	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
45	24, 44	eqeq12d 2781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ↔ (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤))))
46	11, 12	grpcl 18998	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
47	10, 46	syl3an1 1179	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
48	3, 26, 7, 47	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
49	48, 6	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ 𝐵)
50	17	oveqrspc2v 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(+_g‘𝐾)𝑣) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
51	1, 49, 8, 50	syl12anc 849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
52	20	oveqrspc2v 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
53	52	ad2ant2r 759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
54	53	oveq1d 7415	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
55	51, 54	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
56	28, 30	sgrpcl 18774	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
57	25, 7, 9, 56	syl3anc 1394	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
58	57, 6	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)
59	20	oveqrspc2v 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
60	1, 36, 58, 59	syl12anc 849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
61	17	oveqrspc2v 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
62	1, 4, 8, 61	syl12anc 849	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
63	42, 62	oveq12d 7418	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
64	60, 63	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
65	55, 64	eqeq12d 2781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) ↔ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))
66	45, 65	anbi12d 643	. . . . . . . . 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 472	. . . . . . . 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 3186	. . . . . . 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 3227	. . . . . 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 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐾))
71	70	raleqdv 3323	. . . . . . . 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 3339	. . . . . . 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 3339	. . . . . 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 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐿))
76	75	raleqdv 3323	. . . . . . . 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 3339	. . . . . . 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 3339	. . . . . 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 312	. . . . 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 589	. . . 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 1103	. . . 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 1103	. . . 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 317	. . 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 19853	. . . 4 ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
85		fvexd 6886	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ V)
86		fvexd 6886	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐿) ∈ V)
87	28	a1i 11	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
88		eqid 2765	. . . . . . . 8 ⊢ (mulGrp‘𝐿) = (mulGrp‘𝐿)
89		eqid 2765	. . . . . . . 8 ⊢ (Base‘𝐿) = (Base‘𝐿)
90	88, 89	mgpbas 20212	. . . . . . 7 ⊢ (Base‘𝐿) = (Base‘(mulGrp‘𝐿))
91	74, 90	eqtrdi 2816	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘(mulGrp‘𝐿)))
92	5, 91	eqtr3d 2802	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐿)))
93	17	ex 417	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
94	5	eleq2d 2851	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾)))
95	5	eleq2d 2851	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐾)))
96	94, 95	anbi12d 643	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))))
97	96	bicomd 226	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
98	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐾) = (+_g‘(mulGrp‘𝐾)))
99	98	eqcomd 2771	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾))
100	99	oveqd 7417	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(._r‘𝐾)𝑦))
101		eqid 2765	. . . . . . . . . . . 12 ⊢ (._r‘𝐿) = (._r‘𝐿)
102	88, 101	mgpplusg 20211	. . . . . . . . . . 11 ⊢ (._r‘𝐿) = (+_g‘(mulGrp‘𝐿))
103	102	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐿) = (+_g‘(mulGrp‘𝐿)))
104	103	eqcomd 2771	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐿)) = (._r‘𝐿))
105	104	oveqd 7417	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐿))𝑦) = (𝑥(._r‘𝐿)𝑦))
106	100, 105	eqeq12d 2781	. . . . . . 7 ⊢ (𝜑 → ((𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦) ↔ (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
107	93, 97, 106	3imtr4d 297	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦)))
108	107	imp 411	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
109	85, 86, 87, 92, 108	sgrppropd 18779	. . . 4 ⊢ (𝜑 → ((mulGrp‘𝐾) ∈ Smgrp ↔ (mulGrp‘𝐿) ∈ Smgrp))
110	84, 109	3anbi12d 1461	. . 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 282	. 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 20223	. 2 ⊢ (𝐾 ∈ Rng ↔ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
113		eqid 2765	. . 3 ⊢ (+_g‘𝐿) = (+_g‘𝐿)
114	89, 88, 113, 101	isrng 20223	. 2 ⊢ (𝐿 ∈ Rng ↔ (𝐿 ∈ Abel ∧ (mulGrp‘𝐿) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐿)∀𝑣 ∈ (Base‘𝐿)∀𝑤 ∈ (Base‘𝐿)((𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)) ∧ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))))
115	111, 112, 114	3bitr4g 317	1 ⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 Vcvv 3457 ‘cfv 6525 (class class class)co 7400 Basecbs 17259 +_gcplusg 17300 ._rcmulr 17301 Smgrpcsgrp 18766 Grpcgrp 18990 Abelcabl 19842 mulGrpcmgp 20207 Rngcrng 20221

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-plusg 17313 df-0g 17484 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-grp 18993 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222

This theorem is referenced by: opprrngb 20419 subrngpropd 20644

W3C validator