rngpropd

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)

	Ref	Expression
Hypotheses	rngpropd.1	$⊢ φ \to B = {Base}_{K}$
	rngpropd.2	$⊢ φ \to B = {Base}_{L}$
	rngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	rngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	rngpropd	$⊢ φ \to (K \in Rng \leftrightarrow L \in Rng)$

Proof

Step	Hyp	Ref	Expression
1		rngpropd.1	$⊢ φ \to B = {Base}_{K}$
2		rngpropd.2	$⊢ φ \to B = {Base}_{L}$
3		rngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		rngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5		simpll	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to φ$
6		simprll	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \in B$
7		simplrl	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to K \in Abel$
8		simprlr	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v \in B$
9	1	ad2antrr	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to B = {Base}_{K}$
10	8 9	eleqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v \in {Base}_{K}$
11		simprr	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to w \in B$
12	11 9	eleqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to w \in {Base}_{K}$
13		ablgrp	$⊢ K \in Abel \to K \in Grp$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15		eqid	$⊢ +_{K} = +_{K}$
16	14 15	grpcl	$⊢ (K \in Grp \land v \in {Base}_{K} \land w \in {Base}_{K}) \to v +_{K} w \in {Base}_{K}$
17	13 16	syl3an1	$⊢ (K \in Abel \land v \in {Base}_{K} \land w \in {Base}_{K}) \to v +_{K} w \in {Base}_{K}$
18	7 10 12 17	syl3anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w \in {Base}_{K}$
19	18 9	eleqtrrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w \in B$
20	4	oveqrspc2v	$⊢ (φ \land (u \in B \land v +_{K} w \in B)) \to u \cdot_{K} (v +_{K} w) = u \cdot_{L} (v +_{K} w)$
21	5 6 19 20	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} (v +_{K} w) = u \cdot_{L} (v +_{K} w)$
22	3	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v +_{K} w = v +_{L} w$
23	5 8 11 22	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w = v +_{L} w$
24	23	oveq2d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{L} (v +_{K} w) = u \cdot_{L} (v +_{L} w)$
25	21 24	eqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} (v +_{K} w) = u \cdot_{L} (v +_{L} w)$
26		simplrr	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to {mulGrp}_{K} \in Smgrp$
27	6 9	eleqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \in {Base}_{K}$
28		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
29	28 14	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
30		eqid	$⊢ \cdot_{K} = \cdot_{K}$
31	28 30	mgpplusg	$⊢ \cdot_{K} = +_{{mulGrp}_{K}}$
32	29 31	sgrpcl	$⊢ ({mulGrp}_{K} \in Smgrp \land u \in {Base}_{K} \land v \in {Base}_{K}) \to u \cdot_{K} v \in {Base}_{K}$
33	26 27 10 32	syl3anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v \in {Base}_{K}$
34	33 9	eleqtrrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v \in B$
35	29 31	sgrpcl	$⊢ ({mulGrp}_{K} \in Smgrp \land u \in {Base}_{K} \land w \in {Base}_{K}) \to u \cdot_{K} w \in {Base}_{K}$
36	26 27 12 35	syl3anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w \in {Base}_{K}$
37	36 9	eleqtrrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w \in B$
38	3	oveqrspc2v	$⊢ (φ \land (u \cdot_{K} v \in B \land u \cdot_{K} w \in B)) \to (u \cdot_{K} v) +_{K} (u \cdot_{K} w) = (u \cdot_{K} v) +_{L} (u \cdot_{K} w)$
39	5 34 37 38	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} v) +_{K} (u \cdot_{K} w) = (u \cdot_{K} v) +_{L} (u \cdot_{K} w)$
40	4	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u \cdot_{K} v = u \cdot_{L} v$
41	40	ad2ant2r	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v = u \cdot_{L} v$
42	4	oveqrspc2v	$⊢ (φ \land (u \in B \land w \in B)) \to u \cdot_{K} w = u \cdot_{L} w$
43	5 6 11 42	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w = u \cdot_{L} w$
44	41 43	oveq12d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} v) +_{L} (u \cdot_{K} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w)$
45	39 44	eqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} v) +_{K} (u \cdot_{K} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w)$
46	25 45	eqeq12d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \leftrightarrow u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w))$
47	14 15	grpcl	$⊢ (K \in Grp \land u \in {Base}_{K} \land v \in {Base}_{K}) \to u +_{K} v \in {Base}_{K}$
48	13 47	syl3an1	$⊢ (K \in Abel \land u \in {Base}_{K} \land v \in {Base}_{K}) \to u +_{K} v \in {Base}_{K}$
49	7 27 10 48	syl3anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v \in {Base}_{K}$
50	49 9	eleqtrrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v \in B$
51	4	oveqrspc2v	$⊢ (φ \land (u +_{K} v \in B \land w \in B)) \to (u +_{K} v) \cdot_{K} w = (u +_{K} v) \cdot_{L} w$
52	5 50 11 51	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u +_{K} v) \cdot_{K} w = (u +_{K} v) \cdot_{L} w$
53	3	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u +_{K} v = u +_{L} v$
54	53	ad2ant2r	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v = u +_{L} v$
55	54	oveq1d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u +_{K} v) \cdot_{L} w = (u +_{L} v) \cdot_{L} w$
56	52 55	eqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u +_{K} v) \cdot_{K} w = (u +_{L} v) \cdot_{L} w$
57	29 31	sgrpcl	$⊢ ({mulGrp}_{K} \in Smgrp \land v \in {Base}_{K} \land w \in {Base}_{K}) \to v \cdot_{K} w \in {Base}_{K}$
58	26 10 12 57	syl3anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w \in {Base}_{K}$
59	58 9	eleqtrrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w \in B$
60	3	oveqrspc2v	$⊢ (φ \land (u \cdot_{K} w \in B \land v \cdot_{K} w \in B)) \to (u \cdot_{K} w) +_{K} (v \cdot_{K} w) = (u \cdot_{K} w) +_{L} (v \cdot_{K} w)$
61	5 37 59 60	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} w) +_{K} (v \cdot_{K} w) = (u \cdot_{K} w) +_{L} (v \cdot_{K} w)$
62	4	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v \cdot_{K} w = v \cdot_{L} w$
63	5 8 11 62	syl12anc	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w = v \cdot_{L} w$
64	43 63	oveq12d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} w) +_{L} (v \cdot_{K} w) = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)$
65	61 64	eqtrd	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to (u \cdot_{K} w) +_{K} (v \cdot_{K} w) = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)$
66	56 65	eqeq12d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to ((u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w) \leftrightarrow (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))$
67	46 66	anbi12d	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land ((u \in B \land v \in B) \land w \in B)) \to ((u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
68	67	anassrs	$⊢ (((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land (u \in B \land v \in B)) \land w \in B) \to ((u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
69	68	ralbidva	$⊢ ((φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \land (u \in B \land v \in B)) \to (\forall w \in B (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall w \in B (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
70	69	2ralbidva	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall u \in B \forall v \in B \forall w \in B (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall u \in B \forall v \in B \forall w \in B (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
71	1	adantr	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to B = {Base}_{K}$
72	71	raleqdv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall w \in B (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)))$
73	71 72	raleqbidv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall v \in B \forall w \in B (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)))$
74	71 73	raleqbidv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall u \in B \forall v \in B \forall w \in B (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)))$
75	2	adantr	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to B = {Base}_{L}$
76	75	raleqdv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall w \in B (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)) \leftrightarrow \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
77	75 76	raleqbidv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall v \in B \forall w \in B (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)) \leftrightarrow \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
78	75 77	raleqbidv	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall u \in B \forall v \in B \forall w \in B (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)) \leftrightarrow \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
79	70 74 78	3bitr3d	$⊢ (φ \land (K \in Abel \land {mulGrp}_{K} \in Smgrp)) \to (\forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)) \leftrightarrow \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
80	79	pm5.32da	$⊢ φ \to (((K \in Abel \land {mulGrp}_{K} \in Smgrp) \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w))) \leftrightarrow ((K \in Abel \land {mulGrp}_{K} \in Smgrp) \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))))$
81		df-3an	$⊢ (K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w))) \leftrightarrow ((K \in Abel \land {mulGrp}_{K} \in Smgrp) \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)))$
82		df-3an	$⊢ (K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))) \leftrightarrow ((K \in Abel \land {mulGrp}_{K} \in Smgrp) \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
83	80 81 82	3bitr4g	$⊢ φ \to ((K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w))) \leftrightarrow (K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))))$
84	1 2 3	ablpropd	$⊢ φ \to (K \in Abel \leftrightarrow L \in Abel)$
85		fvexd	$⊢ φ \to {mulGrp}_{K} \in V$
86		fvexd	$⊢ φ \to {mulGrp}_{L} \in V$
87	29	a1i	$⊢ φ \to {Base}_{K} = {Base}_{{mulGrp}_{K}}$
88		eqid	$⊢ {mulGrp}_{L} = {mulGrp}_{L}$
89		eqid	$⊢ {Base}_{L} = {Base}_{L}$
90	88 89	mgpbas	$⊢ {Base}_{L} = {Base}_{{mulGrp}_{L}}$
91	2 90	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{L}}$
92	1 91	eqtr3d	$⊢ φ \to {Base}_{K} = {Base}_{{mulGrp}_{L}}$
93	4	ex	$⊢ φ \to ((x \in B \land y \in B) \to x \cdot_{K} y = x \cdot_{L} y)$
94	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{K})$
95	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{K})$
96	94 95	anbi12d	$⊢ φ \to ((x \in B \land y \in B) \leftrightarrow (x \in {Base}_{K} \land y \in {Base}_{K}))$
97	96	bicomd	$⊢ φ \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \leftrightarrow (x \in B \land y \in B))$
98	31	a1i	$⊢ φ \to \cdot_{K} = +_{{mulGrp}_{K}}$
99	98	eqcomd	$⊢ φ \to +_{{mulGrp}_{K}} = \cdot_{K}$
100	99	oveqd	$⊢ φ \to x +_{{mulGrp}_{K}} y = x \cdot_{K} y$
101		eqid	$⊢ \cdot_{L} = \cdot_{L}$
102	88 101	mgpplusg	$⊢ \cdot_{L} = +_{{mulGrp}_{L}}$
103	102	a1i	$⊢ φ \to \cdot_{L} = +_{{mulGrp}_{L}}$
104	103	eqcomd	$⊢ φ \to +_{{mulGrp}_{L}} = \cdot_{L}$
105	104	oveqd	$⊢ φ \to x +_{{mulGrp}_{L}} y = x \cdot_{L} y$
106	100 105	eqeq12d	$⊢ φ \to (x +_{{mulGrp}_{K}} y = x +_{{mulGrp}_{L}} y \leftrightarrow x \cdot_{K} y = x \cdot_{L} y)$
107	93 97 106	3imtr4d	$⊢ φ \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \to x +_{{mulGrp}_{K}} y = x +_{{mulGrp}_{L}} y)$
108	107	imp	$⊢ (φ \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to x +_{{mulGrp}_{K}} y = x +_{{mulGrp}_{L}} y$
109	85 86 87 92 108	sgrppropd	$⊢ φ \to ({mulGrp}_{K} \in Smgrp \leftrightarrow {mulGrp}_{L} \in Smgrp)$
110	84 109	3anbi12d	$⊢ φ \to ((K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))) \leftrightarrow (L \in Abel \land {mulGrp}_{L} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))))$
111	83 110	bitrd	$⊢ φ \to ((K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w))) \leftrightarrow (L \in Abel \land {mulGrp}_{L} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w))))$
112	14 28 15 30	isrng	$⊢ K \in Rng \leftrightarrow (K \in Abel \land {mulGrp}_{K} \in Smgrp \land \forall u \in {Base}_{K} \forall v \in {Base}_{K} \forall w \in {Base}_{K} (u \cdot_{K} (v +_{K} w) = (u \cdot_{K} v) +_{K} (u \cdot_{K} w) \land (u +_{K} v) \cdot_{K} w = (u \cdot_{K} w) +_{K} (v \cdot_{K} w)))$
113		eqid	$⊢ +_{L} = +_{L}$
114	89 88 113 101	isrng	$⊢ L \in Rng \leftrightarrow (L \in Abel \land {mulGrp}_{L} \in Smgrp \land \forall u \in {Base}_{L} \forall v \in {Base}_{L} \forall w \in {Base}_{L} (u \cdot_{L} (v +_{L} w) = (u \cdot_{L} v) +_{L} (u \cdot_{L} w) \land (u +_{L} v) \cdot_{L} w = (u \cdot_{L} w) +_{L} (v \cdot_{L} w)))$
115	111 112 114	3bitr4g	$⊢ φ \to (K \in Rng \leftrightarrow L \in Rng)$

Metamath Proof Explorer

Theorem rngpropd

Proof