iscringd

Description: Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	iscringd.1	$⊢ φ \to G \in AbelOp$
	iscringd.2	$⊢ φ \to X = ran G$
	iscringd.3	$⊢ φ \to H : X \times X ⟶ X$
	iscringd.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x H y) H z = x H (y H z)$
	iscringd.5	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (x H y) G (x H z)$
	iscringd.6	$⊢ φ \to U \in X$
	iscringd.7	$⊢ (φ \land y \in X) \to y H U = y$
	iscringd.8	$⊢ (φ \land (x \in X \land y \in X)) \to x H y = y H x$
Assertion	iscringd	$⊢ φ \to ⟨G, H⟩ \in CRingOps$

Proof

Step	Hyp	Ref	Expression
1		iscringd.1	$⊢ φ \to G \in AbelOp$
2		iscringd.2	$⊢ φ \to X = ran G$
3		iscringd.3	$⊢ φ \to H : X \times X ⟶ X$
4		iscringd.4	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x H y) H z = x H (y H z)$
5		iscringd.5	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (x H y) G (x H z)$
6		iscringd.6	$⊢ φ \to U \in X$
7		iscringd.7	$⊢ (φ \land y \in X) \to y H U = y$
8		iscringd.8	$⊢ (φ \land (x \in X \land y \in X)) \to x H y = y H x$
9		id	$⊢ (z \in X \land y \in X \land x \in X) \to (z \in X \land y \in X \land x \in X)$
10	9	3com13	$⊢ (x \in X \land y \in X \land z \in X) \to (z \in X \land y \in X \land x \in X)$
11		eleq1	$⊢ w = z \to (w \in X \leftrightarrow z \in X)$
12	11	3anbi1d	$⊢ w = z \to ((w \in X \land y \in X \land x \in X) \leftrightarrow (z \in X \land y \in X \land x \in X))$
13	12	anbi2d	$⊢ w = z \to ((φ \land (w \in X \land y \in X \land x \in X)) \leftrightarrow (φ \land (z \in X \land y \in X \land x \in X)))$
14		oveq2	$⊢ w = z \to (x G y) H w = (x G y) H z$
15		oveq2	$⊢ w = z \to x H w = x H z$
16		oveq2	$⊢ w = z \to y H w = y H z$
17	15 16	oveq12d	$⊢ w = z \to (x H w) G (y H w) = (x H z) G (y H z)$
18	14 17	eqeq12d	$⊢ w = z \to ((x G y) H w = (x H w) G (y H w) \leftrightarrow (x G y) H z = (x H z) G (y H z))$
19	13 18	imbi12d	$⊢ w = z \to (((φ \land (w \in X \land y \in X \land x \in X)) \to (x G y) H w = (x H w) G (y H w)) \leftrightarrow ((φ \land (z \in X \land y \in X \land x \in X)) \to (x G y) H z = (x H z) G (y H z)))$
20		eleq1	$⊢ z = x \to (z \in X \leftrightarrow x \in X)$
21	20	3anbi3d	$⊢ z = x \to ((w \in X \land y \in X \land z \in X) \leftrightarrow (w \in X \land y \in X \land x \in X))$
22	21	anbi2d	$⊢ z = x \to ((φ \land (w \in X \land y \in X \land z \in X)) \leftrightarrow (φ \land (w \in X \land y \in X \land x \in X)))$
23		oveq1	$⊢ z = x \to z G y = x G y$
24	23	oveq1d	$⊢ z = x \to (z G y) H w = (x G y) H w$
25		oveq1	$⊢ z = x \to z H w = x H w$
26	25	oveq1d	$⊢ z = x \to (z H w) G (y H w) = (x H w) G (y H w)$
27	24 26	eqeq12d	$⊢ z = x \to ((z G y) H w = (z H w) G (y H w) \leftrightarrow (x G y) H w = (x H w) G (y H w))$
28	22 27	imbi12d	$⊢ z = x \to (((φ \land (w \in X \land y \in X \land z \in X)) \to (z G y) H w = (z H w) G (y H w)) \leftrightarrow ((φ \land (w \in X \land y \in X \land x \in X)) \to (x G y) H w = (x H w) G (y H w)))$
29		eleq1	$⊢ x = w \to (x \in X \leftrightarrow w \in X)$
30	29	3anbi1d	$⊢ x = w \to ((x \in X \land y \in X \land z \in X) \leftrightarrow (w \in X \land y \in X \land z \in X))$
31	30	anbi2d	$⊢ x = w \to ((φ \land (x \in X \land y \in X \land z \in X)) \leftrightarrow (φ \land (w \in X \land y \in X \land z \in X)))$
32		oveq2	$⊢ x = w \to (z G y) H x = (z G y) H w$
33		oveq2	$⊢ x = w \to z H x = z H w$
34		oveq2	$⊢ x = w \to y H x = y H w$
35	33 34	oveq12d	$⊢ x = w \to (z H x) G (y H x) = (z H w) G (y H w)$
36	32 35	eqeq12d	$⊢ x = w \to ((z G y) H x = (z H x) G (y H x) \leftrightarrow (z G y) H w = (z H w) G (y H w))$
37	31 36	imbi12d	$⊢ x = w \to (((φ \land (x \in X \land y \in X \land z \in X)) \to (z G y) H x = (z H x) G (y H x)) \leftrightarrow ((φ \land (w \in X \land y \in X \land z \in X)) \to (z G y) H w = (z H w) G (y H w)))$
38	1	adantr	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to G \in AbelOp$
39		simpr3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z \in X$
40	2	adantr	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to X = ran G$
41	39 40	eleqtrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z \in ran G$
42		simpr2	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y \in X$
43	42 40	eleqtrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y \in ran G$
44		eqid	$⊢ ran G = ran G$
45	44	ablocom	$⊢ (G \in AbelOp \land z \in ran G \land y \in ran G) \to z G y = y G z$
46	38 41 43 45	syl3anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z G y = y G z$
47	46	oveq1d	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (z G y) H x = (y G z) H x$
48		simpr1	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x \in X$
49		ablogrpo	$⊢ G \in AbelOp \to G \in GrpOp$
50	38 49	syl	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to G \in GrpOp$
51	44	grpocl	$⊢ (G \in GrpOp \land y \in ran G \land z \in ran G) \to y G z \in ran G$
52	50 43 41 51	syl3anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y G z \in ran G$
53	52 40	eleqtrrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y G z \in X$
54	48 53	jca	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x \in X \land y G z \in X)$
55		ovex	$⊢ y G z \in V$
56		eleq1	$⊢ w = y G z \to (w \in X \leftrightarrow y G z \in X)$
57	56	anbi2d	$⊢ w = y G z \to ((x \in X \land w \in X) \leftrightarrow (x \in X \land y G z \in X))$
58	57	anbi2d	$⊢ w = y G z \to ((φ \land (x \in X \land w \in X)) \leftrightarrow (φ \land (x \in X \land y G z \in X)))$
59		oveq2	$⊢ w = y G z \to x H w = x H (y G z)$
60		oveq1	$⊢ w = y G z \to w H x = (y G z) H x$
61	59 60	eqeq12d	$⊢ w = y G z \to (x H w = w H x \leftrightarrow x H (y G z) = (y G z) H x)$
62	58 61	imbi12d	$⊢ w = y G z \to (((φ \land (x \in X \land w \in X)) \to x H w = w H x) \leftrightarrow ((φ \land (x \in X \land y G z \in X)) \to x H (y G z) = (y G z) H x))$
63		eleq1	$⊢ y = w \to (y \in X \leftrightarrow w \in X)$
64	63	anbi2d	$⊢ y = w \to ((x \in X \land y \in X) \leftrightarrow (x \in X \land w \in X))$
65	64	anbi2d	$⊢ y = w \to ((φ \land (x \in X \land y \in X)) \leftrightarrow (φ \land (x \in X \land w \in X)))$
66		oveq2	$⊢ y = w \to x H y = x H w$
67		oveq1	$⊢ y = w \to y H x = w H x$
68	66 67	eqeq12d	$⊢ y = w \to (x H y = y H x \leftrightarrow x H w = w H x)$
69	65 68	imbi12d	$⊢ y = w \to (((φ \land (x \in X \land y \in X)) \to x H y = y H x) \leftrightarrow ((φ \land (x \in X \land w \in X)) \to x H w = w H x))$
70	69 8	chvarvv	$⊢ (φ \land (x \in X \land w \in X)) \to x H w = w H x$
71	55 62 70	vtocl	$⊢ (φ \land (x \in X \land y G z \in X)) \to x H (y G z) = (y G z) H x$
72	54 71	syldan	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (y G z) H x$
73	8	3adantr3	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H y = y H x$
74		eleq1	$⊢ y = z \to (y \in X \leftrightarrow z \in X)$
75	74	anbi2d	$⊢ y = z \to ((x \in X \land y \in X) \leftrightarrow (x \in X \land z \in X))$
76	75	anbi2d	$⊢ y = z \to ((φ \land (x \in X \land y \in X)) \leftrightarrow (φ \land (x \in X \land z \in X)))$
77		oveq2	$⊢ y = z \to x H y = x H z$
78		oveq1	$⊢ y = z \to y H x = z H x$
79	77 78	eqeq12d	$⊢ y = z \to (x H y = y H x \leftrightarrow x H z = z H x)$
80	76 79	imbi12d	$⊢ y = z \to (((φ \land (x \in X \land y \in X)) \to x H y = y H x) \leftrightarrow ((φ \land (x \in X \land z \in X)) \to x H z = z H x))$
81	80 8	chvarvv	$⊢ (φ \land (x \in X \land z \in X)) \to x H z = z H x$
82	81	3adantr2	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H z = z H x$
83	73 82	oveq12d	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x H y) G (x H z) = (y H x) G (z H x)$
84	3	adantr	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to H : X \times X ⟶ X$
85	84 42 48	fovrnd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y H x \in X$
86	85 40	eleqtrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to y H x \in ran G$
87	84 39 48	fovrnd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z H x \in X$
88	87 40	eleqtrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to z H x \in ran G$
89	44	ablocom	$⊢ (G \in AbelOp \land y H x \in ran G \land z H x \in ran G) \to (y H x) G (z H x) = (z H x) G (y H x)$
90	38 86 88 89	syl3anc	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (y H x) G (z H x) = (z H x) G (y H x)$
91	5 83 90	3eqtrd	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to x H (y G z) = (z H x) G (y H x)$
92	47 72 91	3eqtr2d	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (z G y) H x = (z H x) G (y H x)$
93	37 92	chvarvv	$⊢ (φ \land (w \in X \land y \in X \land z \in X)) \to (z G y) H w = (z H w) G (y H w)$
94	28 93	chvarvv	$⊢ (φ \land (w \in X \land y \in X \land x \in X)) \to (x G y) H w = (x H w) G (y H w)$
95	19 94	chvarvv	$⊢ (φ \land (z \in X \land y \in X \land x \in X)) \to (x G y) H z = (x H z) G (y H z)$
96	10 95	sylan2	$⊢ (φ \land (x \in X \land y \in X \land z \in X)) \to (x G y) H z = (x H z) G (y H z)$
97	6	adantr	$⊢ (φ \land y \in X) \to U \in X$
98		oveq1	$⊢ x = U \to x H y = U H y$
99		oveq2	$⊢ x = U \to y H x = y H U$
100	98 99	eqeq12d	$⊢ x = U \to (x H y = y H x \leftrightarrow U H y = y H U)$
101	100	imbi2d	$⊢ x = U \to (((φ \land y \in X) \to x H y = y H x) \leftrightarrow ((φ \land y \in X) \to U H y = y H U))$
102	8	an12s	$⊢ (x \in X \land (φ \land y \in X)) \to x H y = y H x$
103	102	ex	$⊢ x \in X \to ((φ \land y \in X) \to x H y = y H x)$
104	101 103	vtoclga	$⊢ U \in X \to ((φ \land y \in X) \to U H y = y H U)$
105	97 104	mpcom	$⊢ (φ \land y \in X) \to U H y = y H U$
106	105 7	eqtrd	$⊢ (φ \land y \in X) \to U H y = y$
107	1 2 3 4 5 96 6 106 7	isrngod	$⊢ φ \to ⟨G, H⟩ \in RingOps$
108	2	eleq2d	$⊢ φ \to (x \in X \leftrightarrow x \in ran G)$
109	2	eleq2d	$⊢ φ \to (y \in X \leftrightarrow y \in ran G)$
110	108 109	anbi12d	$⊢ φ \to ((x \in X \land y \in X) \leftrightarrow (x \in ran G \land y \in ran G))$
111	110	biimpar	$⊢ (φ \land (x \in ran G \land y \in ran G)) \to (x \in X \land y \in X)$
112	111 8	syldan	$⊢ (φ \land (x \in ran G \land y \in ran G)) \to x H y = y H x$
113	112	ralrimivva	$⊢ φ \to \forall x \in ran G \forall y \in ran G x H y = y H x$
114		rnexg	$⊢ G \in AbelOp \to ran G \in V$
115	1 114	syl	$⊢ φ \to ran G \in V$
116	2 115	eqeltrd	$⊢ φ \to X \in V$
117	116 116	xpexd	$⊢ φ \to X \times X \in V$
118		fex	$⊢ (H : X \times X ⟶ X \land X \times X \in V) \to H \in V$
119	3 117 118	syl2anc	$⊢ φ \to H \in V$
120		iscom2	$⊢ (G \in AbelOp \land H \in V) \to (⟨G, H⟩ \in Com2 \leftrightarrow \forall x \in ran G \forall y \in ran G x H y = y H x)$
121	1 119 120	syl2anc	$⊢ φ \to (⟨G, H⟩ \in Com2 \leftrightarrow \forall x \in ran G \forall y \in ran G x H y = y H x)$
122	113 121	mpbird	$⊢ φ \to ⟨G, H⟩ \in Com2$
123		iscrngo	$⊢ ⟨G, H⟩ \in CRingOps \leftrightarrow (⟨G, H⟩ \in RingOps \land ⟨G, H⟩ \in Com2)$
124	107 122 123	sylanbrc	$⊢ φ \to ⟨G, H⟩ \in CRingOps$

Metamath Proof Explorer

Theorem iscringd

Proof