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 20401

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 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝜑)
2		simprll 791	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ 𝐵)
3		simplrl 789	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐾 ∈ Abel)
4		simprlr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ 𝐵)
5		rngpropd.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = (Base‘𝐾))
6	5	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝐵 = (Base‘𝐾))
7	4, 6	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑣 ∈ (Base‘𝐾))
8		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
9	8, 6	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ (Base‘𝐾))
10		ablgrp 20004	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Abel → 𝐾 ∈ Grp)
11		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
13	11, 12	grpcl 19157	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
14	10, 13	syl3an1 1181	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
15	3, 7, 9, 14	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ (Base‘𝐾))
16	15, 6	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)
17		rngpropd.4	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦))
18	17	oveqrspc2v 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ (𝑣(+_g‘𝐾)𝑤) ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
19	1, 2, 16, 18	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)))
20		rngpropd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝐿)𝑦))
21	20	oveqrspc2v 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
22	1, 4, 8, 21	syl12anc 850	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(+_g‘𝐾)𝑤) = (𝑣(+_g‘𝐿)𝑤))
23	22	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐿)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
24	19, 23	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)))
25		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (mulGrp‘𝐾) ∈ Smgrp)
26	2, 6	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → 𝑢 ∈ (Base‘𝐾))
27		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
28	27, 11	mgpbas 20370	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐾) = (Base‘(mulGrp‘𝐾))
29		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝐾) = (._r‘𝐾)
30	27, 29	mgpplusg 20369	. . . . . . . . . . . . . . . 16 ⊢ (._r‘𝐾) = (+_g‘(mulGrp‘𝐾))
31	28, 30	sgrpcl 18920	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
32	25, 26, 7, 31	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ (Base‘𝐾))
33	32, 6	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) ∈ 𝐵)
34	28, 30	sgrpcl 18920	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
35	25, 26, 9, 34	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
36	35, 6	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)
37	20	oveqrspc2v 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑣) ∈ 𝐵 ∧ (𝑢(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
38	1, 33, 36, 37	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)))
39	17	oveqrspc2v 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
40	39	ad2ant2r 760	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑣) = (𝑢(._r‘𝐿)𝑣))
41	17	oveqrspc2v 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
42	1, 2, 8, 41	syl12anc 850	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(._r‘𝐾)𝑤) = (𝑢(._r‘𝐿)𝑤))
43	40, 42	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
44	38, 43	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤)))
45	24, 44	eqeq12d 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ↔ (𝑢(._r‘𝐿)(𝑣(+_g‘𝐿)𝑤)) = ((𝑢(._r‘𝐿)𝑣)(+_g‘𝐿)(𝑢(._r‘𝐿)𝑤))))
46	11, 12	grpcl 19157	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Grp ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
47	10, 46	syl3an1 1181	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Abel ∧ 𝑢 ∈ (Base‘𝐾) ∧ 𝑣 ∈ (Base‘𝐾)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
48	3, 26, 7, 47	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ (Base‘𝐾))
49	48, 6	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) ∈ 𝐵)
50	17	oveqrspc2v 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(+_g‘𝐾)𝑣) ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
51	1, 49, 8, 50	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤))
52	20	oveqrspc2v 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
53	52	ad2ant2r 760	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑢(+_g‘𝐾)𝑣) = (𝑢(+_g‘𝐿)𝑣))
54	53	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐿)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
55	51, 54	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤))
56	28, 30	sgrpcl 18920	. . . . . . . . . . . . . . 15 ⊢ (((mulGrp‘𝐾) ∈ Smgrp ∧ 𝑣 ∈ (Base‘𝐾) ∧ 𝑤 ∈ (Base‘𝐾)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
57	25, 7, 9, 56	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ (Base‘𝐾))
58	57, 6	eleqtrrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)
59	20	oveqrspc2v 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑢(._r‘𝐾)𝑤) ∈ 𝐵 ∧ (𝑣(._r‘𝐾)𝑤) ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
60	1, 36, 58, 59	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)))
61	17	oveqrspc2v 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
62	1, 4, 8, 61	syl12anc 850	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (𝑣(._r‘𝐾)𝑤) = (𝑣(._r‘𝐿)𝑤))
63	42, 62	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
64	60, 63	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤)))
65	55, 64	eqeq12d 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) ∧ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵)) → (((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)) ↔ ((𝑢(+_g‘𝐿)𝑣)(._r‘𝐿)𝑤) = ((𝑢(._r‘𝐿)𝑤)(+_g‘𝐿)(𝑣(._r‘𝐿)𝑤))))
66	45, 65	anbi12d 644	. . . . . . . . 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 473	. . . . . . . 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 3183	. . . . . . 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 3224	. . . . . 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 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐾))
71	70	raleqdv 3319	. . . . . . . 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 3334	. . . . . . 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 3334	. . . . . 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 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp)) → 𝐵 = (Base‘𝐿))
76	75	raleqdv 3319	. . . . . . . 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 3334	. . . . . . 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 3334	. . . . . 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 590	. . . 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 1105	. . . 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 1105	. . . 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 20011	. . . 4 ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
85		fvexd 6900	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐾) ∈ V)
86		fvexd 6900	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝐿) ∈ V)
87	28	a1i 11	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
88		eqid 2760	. . . . . . . 8 ⊢ (mulGrp‘𝐿) = (mulGrp‘𝐿)
89		eqid 2760	. . . . . . . 8 ⊢ (Base‘𝐿) = (Base‘𝐿)
90	88, 89	mgpbas 20370	. . . . . . 7 ⊢ (Base‘𝐿) = (Base‘(mulGrp‘𝐿))
91	74, 90	eqtrdi 2811	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘(mulGrp‘𝐿)))
92	5, 91	eqtr3d 2797	. . . . 5 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(mulGrp‘𝐿)))
93	17	ex 418	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
94	5	eleq2d 2846	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾)))
95	5	eleq2d 2846	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐾)))
96	94, 95	anbi12d 644	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))))
97	96	bicomd 226	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
98	30	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐾) = (+_g‘(mulGrp‘𝐾)))
99	98	eqcomd 2766	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐾)) = (._r‘𝐾))
100	99	oveqd 7437	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(._r‘𝐾)𝑦))
101		eqid 2760	. . . . . . . . . . . 12 ⊢ (._r‘𝐿) = (._r‘𝐿)
102	88, 101	mgpplusg 20369	. . . . . . . . . . 11 ⊢ (._r‘𝐿) = (+_g‘(mulGrp‘𝐿))
103	102	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (._r‘𝐿) = (+_g‘(mulGrp‘𝐿)))
104	103	eqcomd 2766	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘(mulGrp‘𝐿)) = (._r‘𝐿))
105	104	oveqd 7437	. . . . . . . 8 ⊢ (𝜑 → (𝑥(+_g‘(mulGrp‘𝐿))𝑦) = (𝑥(._r‘𝐿)𝑦))
106	100, 105	eqeq12d 2776	. . . . . . 7 ⊢ (𝜑 → ((𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦) ↔ (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝐿)𝑦)))
107	93, 97, 106	3imtr4d 297	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦)))
108	107	imp 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
109	85, 86, 87, 92, 108	sgrppropd 18925	. . . 4 ⊢ (𝜑 → ((mulGrp‘𝐾) ∈ Smgrp ↔ (mulGrp‘𝐿) ∈ Smgrp))
110	84, 109	3anbi12d 1465	. . 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 20381	. 2 ⊢ (𝐾 ∈ Rng ↔ (𝐾 ∈ Abel ∧ (mulGrp‘𝐾) ∈ Smgrp ∧ ∀𝑢 ∈ (Base‘𝐾)∀𝑣 ∈ (Base‘𝐾)∀𝑤 ∈ (Base‘𝐾)((𝑢(._r‘𝐾)(𝑣(+_g‘𝐾)𝑤)) = ((𝑢(._r‘𝐾)𝑣)(+_g‘𝐾)(𝑢(._r‘𝐾)𝑤)) ∧ ((𝑢(+_g‘𝐾)𝑣)(._r‘𝐾)𝑤) = ((𝑢(._r‘𝐾)𝑤)(+_g‘𝐾)(𝑣(._r‘𝐾)𝑤)))))
113		eqid 2760	. . 3 ⊢ (+_g‘𝐿) = (+_g‘𝐿)
114	89, 88, 113, 101	isrng 20381	. 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 Vcvv 3450 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 +_gcplusg 17433 ._rcmulr 17434 Smgrpcsgrp 18912 Grpcgrp 19149 Abelcabl 20000 mulGrpcmgp 20365 Rngcrng 20379

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-nn 12339 df-2 12408 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-plusg 17446 df-0g 17617 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-grp 19152 df-cmn 20001 df-abl 20002 df-mgp 20366 df-rng 20380

This theorem is used by: opprrngb 20581 subrngpropd 20825

W3C validator