ringpropd

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 ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014) (Revised by Mario Carneiro, 6-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ringpropd.1	$⊢ φ \to B = {Base}_{K}$
2		ringpropd.2	$⊢ φ \to B = {Base}_{L}$
3		ringpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		ringpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5		simpll	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to φ$
6		simprll	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \in B$
7		simplrl	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to K \in Grp$
8		simprlr	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v \in B$
9	1	ad2antrr	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to B = {Base}_{K}$
10	8 9	eleqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v \in {Base}_{K}$
11		simprr	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to w \in B$
12	11 9	eleqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to w \in {Base}_{K}$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14		eqid	$⊢ +_{K} = +_{K}$
15	13 14	grpcl	$⊢ (K \in Grp \land v \in {Base}_{K} \land w \in {Base}_{K}) \to v +_{K} w \in {Base}_{K}$
16	7 10 12 15	syl3anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w \in {Base}_{K}$
17	16 9	eleqtrrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w \in B$
18	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)$
19	5 6 17 18	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
20	3	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v +_{K} w = v +_{L} w$
21	5 8 11 20	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v +_{K} w = v +_{L} w$
22	21	oveq2d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
23	19 22	eqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
24		simplrr	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to {mulGrp}_{K} \in Mnd$
25	6 9	eleqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \in {Base}_{K}$
26		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
27	26 13	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
28		eqid	$⊢ \cdot_{K} = \cdot_{K}$
29	26 28	mgpplusg	$⊢ \cdot_{K} = +_{{mulGrp}_{K}}$
30	27 29	mndcl	$⊢ ({mulGrp}_{K} \in Mnd \land u \in {Base}_{K} \land v \in {Base}_{K}) \to u \cdot_{K} v \in {Base}_{K}$
31	24 25 10 30	syl3anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v \in {Base}_{K}$
32	31 9	eleqtrrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v \in B$
33	27 29	mndcl	$⊢ ({mulGrp}_{K} \in Mnd \land u \in {Base}_{K} \land w \in {Base}_{K}) \to u \cdot_{K} w \in {Base}_{K}$
34	24 25 12 33	syl3anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w \in {Base}_{K}$
35	34 9	eleqtrrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w \in B$
36	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)$
37	5 32 35 36	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
38	4	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u \cdot_{K} v = u \cdot_{L} v$
39	5 6 8 38	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} v = u \cdot_{L} v$
40	4	oveqrspc2v	$⊢ (φ \land (u \in B \land w \in B)) \to u \cdot_{K} w = u \cdot_{L} w$
41	5 6 11 40	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u \cdot_{K} w = u \cdot_{L} w$
42	39 41	oveq12d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
43	37 42	eqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
44	23 43	eqeq12d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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))$
45	13 14	grpcl	$⊢ (K \in Grp \land u \in {Base}_{K} \land v \in {Base}_{K}) \to u +_{K} v \in {Base}_{K}$
46	7 25 10 45	syl3anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v \in {Base}_{K}$
47	46 9	eleqtrrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v \in B$
48	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$
49	5 47 11 48	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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$
50	3	oveqrspc2v	$⊢ (φ \land (u \in B \land v \in B)) \to u +_{K} v = u +_{L} v$
51	5 6 8 50	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to u +_{K} v = u +_{L} v$
52	51	oveq1d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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$
53	49 52	eqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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$
54	27 29	mndcl	$⊢ ({mulGrp}_{K} \in Mnd \land v \in {Base}_{K} \land w \in {Base}_{K}) \to v \cdot_{K} w \in {Base}_{K}$
55	24 10 12 54	syl3anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w \in {Base}_{K}$
56	55 9	eleqtrrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w \in B$
57	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)$
58	5 35 56 57	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
59	4	oveqrspc2v	$⊢ (φ \land (v \in B \land w \in B)) \to v \cdot_{K} w = v \cdot_{L} w$
60	5 8 11 59	syl12anc	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \land ((u \in B \land v \in B) \land w \in B)) \to v \cdot_{K} w = v \cdot_{L} w$
61	41 60	oveq12d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
62	58 61	eqtrd	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)$
63	53 62	eqeq12d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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))$
64	44 63	anbi12d	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
65	64	anassrs	$⊢ (((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
66	65	ralbidva	$⊢ ((φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
67	66	2ralbidva	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
68	1	adantr	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \to B = {Base}_{K}$
69	68	raleqdv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
70	68 69	raleqbidv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
71	68 70	raleqbidv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
72	2	adantr	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \to B = {Base}_{L}$
73	72	raleqdv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
74	72 73	raleqbidv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
75	72 74	raleqbidv	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
76	67 71 75	3bitr3d	$⊢ (φ \land (K \in Grp \land {mulGrp}_{K} \in Mnd)) \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)))$
77	76	pm5.32da	$⊢ φ \to (((K \in Grp \land {mulGrp}_{K} \in Mnd) \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 Grp \land {mulGrp}_{K} \in Mnd) \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))))$
78		df-3an	$⊢ (K \in Grp \land {mulGrp}_{K} \in Mnd \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 Grp \land {mulGrp}_{K} \in Mnd) \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)))$
79		df-3an	$⊢ (K \in Grp \land {mulGrp}_{K} \in Mnd \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 Grp \land {mulGrp}_{K} \in Mnd) \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)))$
80	77 78 79	3bitr4g	$⊢ φ \to ((K \in Grp \land {mulGrp}_{K} \in Mnd \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 Grp \land {mulGrp}_{K} \in Mnd \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	1 2 3	grppropd	$⊢ φ \to (K \in Grp \leftrightarrow L \in Grp)$
82	1 27	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{K}}$
83		eqid	$⊢ {mulGrp}_{L} = {mulGrp}_{L}$
84		eqid	$⊢ {Base}_{L} = {Base}_{L}$
85	83 84	mgpbas	$⊢ {Base}_{L} = {Base}_{{mulGrp}_{L}}$
86	2 85	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{L}}$
87	29	oveqi	$⊢ x \cdot_{K} y = x +_{{mulGrp}_{K}} y$
88		eqid	$⊢ \cdot_{L} = \cdot_{L}$
89	83 88	mgpplusg	$⊢ \cdot_{L} = +_{{mulGrp}_{L}}$
90	89	oveqi	$⊢ x \cdot_{L} y = x +_{{mulGrp}_{L}} y$
91	4 87 90	3eqtr3g	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{{mulGrp}_{K}} y = x +_{{mulGrp}_{L}} y$
92	82 86 91	mndpropd	$⊢ φ \to ({mulGrp}_{K} \in Mnd \leftrightarrow {mulGrp}_{L} \in Mnd)$
93	81 92	3anbi12d	$⊢ φ \to ((K \in Grp \land {mulGrp}_{K} \in Mnd \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 Grp \land {mulGrp}_{L} \in Mnd \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))))$
94	80 93	bitrd	$⊢ φ \to ((K \in Grp \land {mulGrp}_{K} \in Mnd \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 Grp \land {mulGrp}_{L} \in Mnd \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))))$
95	13 26 14 28	isring	$⊢ K \in Ring \leftrightarrow (K \in Grp \land {mulGrp}_{K} \in Mnd \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)))$
96		eqid	$⊢ +_{L} = +_{L}$
97	84 83 96 88	isring	$⊢ L \in Ring \leftrightarrow (L \in Grp \land {mulGrp}_{L} \in Mnd \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)))$
98	94 95 97	3bitr4g	$⊢ φ \to (K \in Ring \leftrightarrow L \in Ring)$

Metamath Proof Explorer

Theorem ringpropd

Proof