Theorem ringi 8138

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.)

Hypotheses

Ref	Expression
ringi.1	⊢ G = (1st ‘R)
ringi.2	⊢ H = (2nd ‘R)
ringi.3	⊢ X = ran G

Assertion

Ref	Expression
ringi	⊢ (R ∈ Ring → ((G ∈ Abel ⋀ H:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz))) ⋀ ∃x ∈ X ∀y ∈ X ((yHx) = y ⋀ (xHy) = y))))

Distinct variable groups:   x,G,y,z   x,H,y,z   x,X,y,z

Proof of Theorem ringi

Step	Hyp	Ref	Expression
1		df-ring 8136	. . 3 ⊢ Ring = {⟨g, h⟩∣((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ⋀ (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ⋀ ∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y)))}
2	1	eleq2i 1541	. 2 ⊢ (R ∈ Ring ↔ R ∈ {⟨g, h⟩∣((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ⋀ (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ⋀ ∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y)))})
3		ringi.1	. . . . 5 ⊢ G = (1st ‘R)
4	3	eqeq2i 1488	. . . 4 ⊢ (g = G ↔ g = (1st ‘R))
5		eleq1 1537	. . . . . 6 ⊢ (g = G → (g ∈ Abel ↔ G ∈ Abel))
6		rneq 3345	. . . . . . . 8 ⊢ (g = G → ran g = ran G)
7		ringi.3	. . . . . . . 8 ⊢ X = ran G
8	6, 7	syl6eqr 1528	. . . . . . 7 ⊢ (g = G → ran g = X)
9		xpeq1 3206	. . . . . . . . . 10 ⊢ (ran g = X → (ran g × ran g) = (X × ran g))
10		xpeq2 3207	. . . . . . . . . 10 ⊢ (ran g = X → (X × ran g) = (X × X))
11	9, 10	eqtrd 1510	. . . . . . . . 9 ⊢ (ran g = X → (ran g × ran g) = (X × X))
12		feq2 3627	. . . . . . . . 9 ⊢ ((ran g × ran g) = (X × X) → (h:(ran g × ran g)–→ran g ↔ h:(X × X)–→ran g))
13	11, 12	syl 10	. . . . . . . 8 ⊢ (ran g = X → (h:(ran g × ran g)–→ran g ↔ h:(X × X)–→ran g))
14		feq3 3628	. . . . . . . 8 ⊢ (ran g = X → (h:(X × X)–→ran g ↔ h:(X × X)–→X))
15	13, 14	bitrd 530	. . . . . . 7 ⊢ (ran g = X → (h:(ran g × ran g)–→ran g ↔ h:(X × X)–→X))
16	8, 15	syl 10	. . . . . 6 ⊢ (g = G → (h:(ran g × ran g)–→ran g ↔ h:(X × X)–→X))
17	5, 16	anbi12d 630	. . . . 5 ⊢ (g = G → ((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ↔ (G ∈ Abel ⋀ h:(X × X)–→X)))
18		raleq1 1789	. . . . . . . . . 10 ⊢ (ran g = X → (∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz)))))
19	18	raleqd 1794	. . . . . . . . 9 ⊢ (ran g = X → (∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz)))))
20	19	raleqd 1794	. . . . . . . 8 ⊢ (ran g = X → (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz)))))
21	8, 20	syl 10	. . . . . . 7 ⊢ (g = G → (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz)))))
22		opreq 3973	. . . . . . . . . . . 12 ⊢ (g = G → (ygz) = (yGz))
23	22	opreq2d 3982	. . . . . . . . . . 11 ⊢ (g = G → (xh(ygz)) = (xh(yGz)))
24		opreq 3973	. . . . . . . . . . 11 ⊢ (g = G → ((xhy)g(xhz)) = ((xhy)G(xhz)))
25	23, 24	eqeq12d 1492	. . . . . . . . . 10 ⊢ (g = G → ((xh(ygz)) = ((xhy)g(xhz)) ↔ (xh(yGz)) = ((xhy)G(xhz))))
26		opreq 3973	. . . . . . . . . . . 12 ⊢ (g = G → (xgy) = (xGy))
27	26	opreq1d 3981	. . . . . . . . . . 11 ⊢ (g = G → ((xgy)hz) = ((xGy)hz))
28		opreq 3973	. . . . . . . . . . 11 ⊢ (g = G → ((xhz)g(yhz)) = ((xhz)G(yhz)))
29	27, 28	eqeq12d 1492	. . . . . . . . . 10 ⊢ (g = G → (((xgy)hz) = ((xhz)g(yhz)) ↔ ((xGy)hz) = ((xhz)G(yhz))))
30	25, 29	3anbi23d 898	. . . . . . . . 9 ⊢ (g = G → ((((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz)))))
31	30	ralbidv 1666	. . . . . . . 8 ⊢ (g = G → (∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz)))))
32	31	2ralbidv 1683	. . . . . . 7 ⊢ (g = G → (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz)))))
33	21, 32	bitrd 530	. . . . . 6 ⊢ (g = G → (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ↔ ∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz)))))
34	8	raleq1d 1792	. . . . . . 7 ⊢ (g = G → (∀y ∈ ran g((yhx) = y ⋀ (xhy) = y) ↔ ∀y ∈ X ((yhx) = y ⋀ (xhy) = y)))
35	8, 34	rexeq12d 1798	. . . . . 6 ⊢ (g = G → (∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y) ↔ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y)))
36	33, 35	anbi12d 630	. . . . 5 ⊢ (g = G → ((∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ⋀ ∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y)) ↔ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y))))
37	17, 36	anbi12d 630	. . . 4 ⊢ (g = G → (((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ⋀ (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ⋀ ∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y))) ↔ ((G ∈ Abel ⋀ h:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y)))))
38	4, 37	sylbir 201	. . 3 ⊢ (g = (1st ‘R) → (((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ⋀ (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xhy)hz) = (xh(yhz)) ⋀ (xh(ygz)) = ((xhy)g(xhz)) ⋀ ((xgy)hz) = ((xhz)g(yhz))) ⋀ ∃x ∈ ran g∀y ∈ ran g((yhx) = y ⋀ (xhy) = y))) ↔ ((G ∈ Abel ⋀ h:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y)))))
39		ringi.2	. . . . 5 ⊢ H = (2nd ‘R)
40	39	eqeq2i 1488	. . . 4 ⊢ (h = H ↔ h = (2nd ‘R))
41		feq1 3626	. . . . . 6 ⊢ (h = H → (h:(X × X)–→X ↔ H:(X × X)–→X))
42	41	anbi2d 618	. . . . 5 ⊢ (h = H → ((G ∈ Abel ⋀ h:(X × X)–→X) ↔ (G ∈ Abel ⋀ H:(X × X)–→X)))
43		opreq 3973	. . . . . . . . . . 11 ⊢ (h = H → ((xhy)hz) = ((xhy)Hz))
44		opreq 3973	. . . . . . . . . . . 12 ⊢ (h = H → (xhy) = (xHy))
45	44	opreq1d 3981	. . . . . . . . . . 11 ⊢ (h = H → ((xhy)Hz) = ((xHy)Hz))
46	43, 45	eqtrd 1510	. . . . . . . . . 10 ⊢ (h = H → ((xhy)hz) = ((xHy)Hz))
47		opreq 3973	. . . . . . . . . . 11 ⊢ (h = H → (xh(yhz)) = (xH(yhz)))
48		opreq 3973	. . . . . . . . . . . 12 ⊢ (h = H → (yhz) = (yHz))
49	48	opreq2d 3982	. . . . . . . . . . 11 ⊢ (h = H → (xH(yhz)) = (xH(yHz)))
50	47, 49	eqtrd 1510	. . . . . . . . . 10 ⊢ (h = H → (xh(yhz)) = (xH(yHz)))
51	46, 50	eqeq12d 1492	. . . . . . . . 9 ⊢ (h = H → (((xhy)hz) = (xh(yhz)) ↔ ((xHy)Hz) = (xH(yHz))))
52		opreq 3973	. . . . . . . . . 10 ⊢ (h = H → (xh(yGz)) = (xH(yGz)))
53		opreq 3973	. . . . . . . . . . 11 ⊢ (h = H → (xhz) = (xHz))
54	44, 53	opreq12d 3984	. . . . . . . . . 10 ⊢ (h = H → ((xhy)G(xhz)) = ((xHy)G(xHz)))
55	52, 54	eqeq12d 1492	. . . . . . . . 9 ⊢ (h = H → ((xh(yGz)) = ((xhy)G(xhz)) ↔ (xH(yGz)) = ((xHy)G(xHz))))
56		opreq 3973	. . . . . . . . . 10 ⊢ (h = H → ((xGy)hz) = ((xGy)Hz))
57	53, 48	opreq12d 3984	. . . . . . . . . 10 ⊢ (h = H → ((xhz)G(yhz)) = ((xHz)G(yHz)))
58	56, 57	eqeq12d 1492	. . . . . . . . 9 ⊢ (h = H → (((xGy)hz) = ((xhz)G(yhz)) ↔ ((xGy)Hz) = ((xHz)G(yHz))))
59	51, 55, 58	3anbi123d 895	. . . . . . . 8 ⊢ (h = H → ((((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ↔ (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz)))))
60	59	ralbidv 1666	. . . . . . 7 ⊢ (h = H → (∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ↔ ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz)))))
61	60	2ralbidv 1683	. . . . . 6 ⊢ (h = H → (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ↔ ∀x ∈ X ∀y ∈ X ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz)))))
62		opreq 3973	. . . . . . . . 9 ⊢ (h = H → (yhx) = (yHx))
63	62	eqeq1d 1486	. . . . . . . 8 ⊢ (h = H → ((yhx) = y ↔ (yHx) = y))
64	44	eqeq1d 1486	. . . . . . . 8 ⊢ (h = H → ((xhy) = y ↔ (xHy) = y))
65	63, 64	anbi12d 630	. . . . . . 7 ⊢ (h = H → (((yhx) = y ⋀ (xhy) = y) ↔ ((yHx) = y ⋀ (xHy) = y)))
66	65	rexralbidv 1685	. . . . . 6 ⊢ (h = H → (∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y) ↔ ∃x ∈ X ∀y ∈ X ((yHx) = y ⋀ (xHy) = y)))
67	61, 66	anbi12d 630	. . . . 5 ⊢ (h = H → ((∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y)) ↔ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz))) ⋀ ∃x ∈ X ∀y ∈ X ((yHx) = y ⋀ (xHy) = y))))
68	42, 67	anbi12d 630	. . . 4 ⊢ (h = H → (((G ∈ Abel ⋀ h:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y))) ↔ ((G ∈ Abel ⋀ H:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz))) ⋀ ∃x ∈ X ∀y ∈ X ((yHx) = y ⋀ (xHy) = y)))))
69	40, 68	sylbir 201	. . 3 ⊢ (h = (2nd ‘R) → (((G ∈ Abel ⋀ h:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xhy)hz) = (xh(yhz)) ⋀ (xh(yGz)) = ((xhy)G(xhz)) ⋀ ((xGy)hz) = ((xhz)G(yhz))) ⋀ ∃x ∈ X ∀y ∈ X ((yhx) = y ⋀ (xhy) = y))) ↔ ((G ∈ Abel ⋀ H:(X × X)–→X) ⋀ (∀x ∈ X ∀y ∈ X ∀z ∈ X (((xHy)Hz) = (xH(yHz)) ⋀ (xH(yGz)) = ((xHy)G(xHz)) ⋀ ((xGy)Hz) = ((xHz)G(yHz))) ⋀ ∃x ∈ X ∀y ∈ X ((yHx) = y ⋀ (xHy) = y)))))
70	38, 69	elopabi 4123	. 2 ⊢ (R ∈ {⟨g, h⟩∣((g ∈ Abel ⋀ h:(ran g × ran g)–→ran g) ⋀ (∀x ∈ ran g∀y ∈ ran g∀z ∈ ran g(((xh