rhmpropd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > rhmpropd		GIF version

Theorem rhmpropd 14183

Description: Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)

**Hypotheses**
Ref	Expression
rhmpropd.a	⊢ (𝜑 → 𝐵 = (Base‘𝐽))
rhmpropd.b	⊢ (𝜑 → 𝐶 = (Base‘𝐾))
rhmpropd.c	⊢ (𝜑 → 𝐵 = (Base‘𝐿))
rhmpropd.d	⊢ (𝜑 → 𝐶 = (Base‘𝑀))
rhmpropd.e	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐽)𝑦) = (𝑥(+_g‘𝐿)𝑦))
rhmpropd.f	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝑀)𝑦))
rhmpropd.g	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐽)𝑦) = (𝑥(._r‘𝐿)𝑦))
rhmpropd.h	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝑀)𝑦))

**Assertion**
Ref	Expression
rhmpropd	⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀))

Distinct variable groups: 𝑥,𝑦,𝐽 𝑥,𝐾,𝑦 𝑥,𝐿,𝑦 𝑥,𝑀,𝑦 𝜑,𝑥,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦

Proof of Theorem rhmpropd Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2209	. . . . . 6 ⊢ (mulGrp‘𝐽) = (mulGrp‘𝐽)
2		eqid 2209	. . . . . 6 ⊢ (mulGrp‘𝐾) = (mulGrp‘𝐾)
3	1, 2	isrhm 14087	. . . . 5 ⊢ (𝑓 ∈ (𝐽 RingHom 𝐾) ↔ ((𝐽 ∈ Ring ∧ 𝐾 ∈ Ring) ∧ (𝑓 ∈ (𝐽 GrpHom 𝐾) ∧ 𝑓 ∈ ((mulGrp‘𝐽) MndHom (mulGrp‘𝐾)))))
4	3	simplbi 274	. . . 4 ⊢ (𝑓 ∈ (𝐽 RingHom 𝐾) → (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring))
5	4	a1i 9	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐽 RingHom 𝐾) → (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)))
6		eqid 2209	. . . . . 6 ⊢ (mulGrp‘𝐿) = (mulGrp‘𝐿)
7		eqid 2209	. . . . . 6 ⊢ (mulGrp‘𝑀) = (mulGrp‘𝑀)
8	6, 7	isrhm 14087	. . . . 5 ⊢ (𝑓 ∈ (𝐿 RingHom 𝑀) ↔ ((𝐿 ∈ Ring ∧ 𝑀 ∈ Ring) ∧ (𝑓 ∈ (𝐿 GrpHom 𝑀) ∧ 𝑓 ∈ ((mulGrp‘𝐿) MndHom (mulGrp‘𝑀)))))
9	8	simplbi 274	. . . 4 ⊢ (𝑓 ∈ (𝐿 RingHom 𝑀) → (𝐿 ∈ Ring ∧ 𝑀 ∈ Ring))
10		rhmpropd.a	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐽))
11		rhmpropd.c	. . . . . 6 ⊢ (𝜑 → 𝐵 = (Base‘𝐿))
12		rhmpropd.e	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘𝐽)𝑦) = (𝑥(+_g‘𝐿)𝑦))
13		rhmpropd.g	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐽)𝑦) = (𝑥(._r‘𝐿)𝑦))
14	10, 11, 12, 13	ringpropd 13967	. . . . 5 ⊢ (𝜑 → (𝐽 ∈ Ring ↔ 𝐿 ∈ Ring))
15		rhmpropd.b	. . . . . 6 ⊢ (𝜑 → 𝐶 = (Base‘𝐾))
16		rhmpropd.d	. . . . . 6 ⊢ (𝜑 → 𝐶 = (Base‘𝑀))
17		rhmpropd.f	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+_g‘𝐾)𝑦) = (𝑥(+_g‘𝑀)𝑦))
18		rhmpropd.h	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝑀)𝑦))
19	15, 16, 17, 18	ringpropd 13967	. . . . 5 ⊢ (𝜑 → (𝐾 ∈ Ring ↔ 𝑀 ∈ Ring))
20	14, 19	anbi12d 473	. . . 4 ⊢ (𝜑 → ((𝐽 ∈ Ring ∧ 𝐾 ∈ Ring) ↔ (𝐿 ∈ Ring ∧ 𝑀 ∈ Ring)))
21	9, 20	imbitrrid 156	. . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐿 RingHom 𝑀) → (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)))
22	20	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → ((𝐽 ∈ Ring ∧ 𝐾 ∈ Ring) ↔ (𝐿 ∈ Ring ∧ 𝑀 ∈ Ring)))
23	10, 15, 11, 16, 12, 17	ghmpropd 13786	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 GrpHom 𝐾) = (𝐿 GrpHom 𝑀))
24	23	eleq2d 2279	. . . . . . . 8 ⊢ (𝜑 → (𝑓 ∈ (𝐽 GrpHom 𝐾) ↔ 𝑓 ∈ (𝐿 GrpHom 𝑀)))
25	24	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (𝑓 ∈ (𝐽 GrpHom 𝐾) ↔ 𝑓 ∈ (𝐿 GrpHom 𝑀)))
26	10	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐵 = (Base‘𝐽))
27		simprl 529	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐽 ∈ Ring)
28		eqid 2209	. . . . . . . . . . . 12 ⊢ (Base‘𝐽) = (Base‘𝐽)
29	1, 28	mgpbasg 13855	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Ring → (Base‘𝐽) = (Base‘(mulGrp‘𝐽)))
30	27, 29	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (Base‘𝐽) = (Base‘(mulGrp‘𝐽)))
31	26, 30	eqtrd 2242	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐵 = (Base‘(mulGrp‘𝐽)))
32	15	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐶 = (Base‘𝐾))
33		simprr 531	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐾 ∈ Ring)
34		eqid 2209	. . . . . . . . . . . 12 ⊢ (Base‘𝐾) = (Base‘𝐾)
35	2, 34	mgpbasg 13855	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Ring → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
36	33, 35	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (Base‘𝐾) = (Base‘(mulGrp‘𝐾)))
37	32, 36	eqtrd 2242	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐶 = (Base‘(mulGrp‘𝐾)))
38	11	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐵 = (Base‘𝐿))
39	20	simprbda 383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐿 ∈ Ring)
40		eqid 2209	. . . . . . . . . . . 12 ⊢ (Base‘𝐿) = (Base‘𝐿)
41	6, 40	mgpbasg 13855	. . . . . . . . . . 11 ⊢ (𝐿 ∈ Ring → (Base‘𝐿) = (Base‘(mulGrp‘𝐿)))
42	39, 41	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (Base‘𝐿) = (Base‘(mulGrp‘𝐿)))
43	38, 42	eqtrd 2242	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐵 = (Base‘(mulGrp‘𝐿)))
44	16	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐶 = (Base‘𝑀))
45	20	simplbda 384	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝑀 ∈ Ring)
46		eqid 2209	. . . . . . . . . . . 12 ⊢ (Base‘𝑀) = (Base‘𝑀)
47	7, 46	mgpbasg 13855	. . . . . . . . . . 11 ⊢ (𝑀 ∈ Ring → (Base‘𝑀) = (Base‘(mulGrp‘𝑀)))
48	45, 47	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (Base‘𝑀) = (Base‘(mulGrp‘𝑀)))
49	44, 48	eqtrd 2242	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → 𝐶 = (Base‘(mulGrp‘𝑀)))
50	13	adantlr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐽)𝑦) = (𝑥(._r‘𝐿)𝑦))
51	27	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐽 ∈ Ring)
52		eqid 2209	. . . . . . . . . . . . 13 ⊢ (._r‘𝐽) = (._r‘𝐽)
53	1, 52	mgpplusgg 13853	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ Ring → (._r‘𝐽) = (+_g‘(mulGrp‘𝐽)))
54	53	oveqd 5991	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Ring → (𝑥(._r‘𝐽)𝑦) = (𝑥(+_g‘(mulGrp‘𝐽))𝑦))
55	51, 54	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐽)𝑦) = (𝑥(+_g‘(mulGrp‘𝐽))𝑦))
56	39	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐿 ∈ Ring)
57		eqid 2209	. . . . . . . . . . . . 13 ⊢ (._r‘𝐿) = (._r‘𝐿)
58	6, 57	mgpplusgg 13853	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ Ring → (._r‘𝐿) = (+_g‘(mulGrp‘𝐿)))
59	58	oveqd 5991	. . . . . . . . . . 11 ⊢ (𝐿 ∈ Ring → (𝑥(._r‘𝐿)𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
60	56, 59	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(._r‘𝐿)𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
61	50, 55, 60	3eqtr3d 2250	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+_g‘(mulGrp‘𝐽))𝑦) = (𝑥(+_g‘(mulGrp‘𝐿))𝑦))
62	18	adantlr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(._r‘𝑀)𝑦))
63	33	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐾 ∈ Ring)
64		eqid 2209	. . . . . . . . . . . . 13 ⊢ (._r‘𝐾) = (._r‘𝐾)
65	2, 64	mgpplusgg 13853	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → (._r‘𝐾) = (+_g‘(mulGrp‘𝐾)))
66	65	oveqd 5991	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Ring → (𝑥(._r‘𝐾)𝑦) = (𝑥(+_g‘(mulGrp‘𝐾))𝑦))
67	63, 66	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(._r‘𝐾)𝑦) = (𝑥(+_g‘(mulGrp‘𝐾))𝑦))
68	45	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑀 ∈ Ring)
69		eqid 2209	. . . . . . . . . . . . 13 ⊢ (._r‘𝑀) = (._r‘𝑀)
70	7, 69	mgpplusgg 13853	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ Ring → (._r‘𝑀) = (+_g‘(mulGrp‘𝑀)))
71	70	oveqd 5991	. . . . . . . . . . 11 ⊢ (𝑀 ∈ Ring → (𝑥(._r‘𝑀)𝑦) = (𝑥(+_g‘(mulGrp‘𝑀))𝑦))
72	68, 71	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(._r‘𝑀)𝑦) = (𝑥(+_g‘(mulGrp‘𝑀))𝑦))
73	62, 67, 72	3eqtr3d 2250	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+_g‘(mulGrp‘𝐾))𝑦) = (𝑥(+_g‘(mulGrp‘𝑀))𝑦))
74	31, 37, 43, 49, 61, 73	mhmpropd 13465	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → ((mulGrp‘𝐽) MndHom (mulGrp‘𝐾)) = ((mulGrp‘𝐿) MndHom (mulGrp‘𝑀)))
75	74	eleq2d 2279	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (𝑓 ∈ ((mulGrp‘𝐽) MndHom (mulGrp‘𝐾)) ↔ 𝑓 ∈ ((mulGrp‘𝐿) MndHom (mulGrp‘𝑀))))
76	25, 75	anbi12d 473	. . . . . 6 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → ((𝑓 ∈ (𝐽 GrpHom 𝐾) ∧ 𝑓 ∈ ((mulGrp‘𝐽) MndHom (mulGrp‘𝐾))) ↔ (𝑓 ∈ (𝐿 GrpHom 𝑀) ∧ 𝑓 ∈ ((mulGrp‘𝐿) MndHom (mulGrp‘𝑀)))))
77	22, 76	anbi12d 473	. . . . 5 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (((𝐽 ∈ Ring ∧ 𝐾 ∈ Ring) ∧ (𝑓 ∈ (𝐽 GrpHom 𝐾) ∧ 𝑓 ∈ ((mulGrp‘𝐽) MndHom (mulGrp‘𝐾)))) ↔ ((𝐿 ∈ Ring ∧ 𝑀 ∈ Ring) ∧ (𝑓 ∈ (𝐿 GrpHom 𝑀) ∧ 𝑓 ∈ ((mulGrp‘𝐿) MndHom (mulGrp‘𝑀))))))
78	77, 3, 8	3bitr4g 223	. . . 4 ⊢ ((𝜑 ∧ (𝐽 ∈ Ring ∧ 𝐾 ∈ Ring)) → (𝑓 ∈ (𝐽 RingHom 𝐾) ↔ 𝑓 ∈ (𝐿 RingHom 𝑀)))
79	78	ex 115	. . 3 ⊢ (𝜑 → ((𝐽 ∈ Ring ∧ 𝐾 ∈ Ring) → (𝑓 ∈ (𝐽 RingHom 𝐾) ↔ 𝑓 ∈ (𝐿 RingHom 𝑀))))
80	5, 21, 79	pm5.21ndd 709	. 2 ⊢ (𝜑 → (𝑓 ∈ (𝐽 RingHom 𝐾) ↔ 𝑓 ∈ (𝐿 RingHom 𝑀)))
81	80	eqrdv 2207	1 ⊢ (𝜑 → (𝐽 RingHom 𝐾) = (𝐿 RingHom 𝑀))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1375 ∈ wcel 2180 ‘cfv 5294 (class class class)co 5974 Basecbs 12998 +_gcplusg 13076 ._rcmulr 13077 MndHom cmhm 13456 GrpHom cghm 13743 mulGrpcmgp 13849 Ringcrg 13925 RingHom crh 14079

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 713 ax-5 1473 ax-7 1474 ax-gen 1475 ax-ie1 1519 ax-ie2 1520 ax-8 1530 ax-10 1531 ax-11 1532 ax-i12 1533 ax-bndl 1535 ax-4 1536 ax-17 1552 ax-i9 1556 ax-ial 1560 ax-i5r 1561 ax-13 2182 ax-14 2183 ax-ext 2191 ax-coll 4178 ax-sep 4181 ax-pow 4237 ax-pr 4272 ax-un 4501 ax-setind 4606 ax-cnex 8058 ax-resscn 8059 ax-1cn 8060 ax-1re 8061 ax-icn 8062 ax-addcl 8063 ax-addrcl 8064 ax-mulcl 8065 ax-addcom 8067 ax-addass 8069 ax-i2m1 8072 ax-0lt1 8073 ax-0id 8075 ax-rnegex 8076 ax-pre-ltirr 8079 ax-pre-ltadd 8083

This theorem depends on definitions: df-bi 117 df-3an 985 df-tru 1378 df-fal 1381 df-nf 1487 df-sb 1789 df-eu 2060 df-mo 2061 df-clab 2196 df-cleq 2202 df-clel 2205 df-nfc 2341 df-ne 2381 df-nel 2476 df-ral 2493 df-rex 2494 df-reu 2495 df-rmo 2496 df-rab 2497 df-v 2781 df-sbc 3009 df-csb 3105 df-dif 3179 df-un 3181 df-in 3183 df-ss 3190 df-nul 3472 df-pw 3631 df-sn 3652 df-pr 3653 df-op 3655 df-uni 3868 df-int 3903 df-iun 3946 df-br 4063 df-opab 4125 df-mpt 4126 df-id 4361 df-xp 4702 df-rel 4703 df-cnv 4704 df-co 4705 df-dm 4706 df-rn 4707 df-res 4708 df-ima 4709 df-iota 5254 df-fun 5296 df-fn 5297 df-f 5298 df-f1 5299 df-fo 5300 df-f1o 5301 df-fv 5302 df-riota 5927 df-ov 5977 df-oprab 5978 df-mpo 5979 df-1st 6256 df-2nd 6257 df-map 6767 df-pnf 8151 df-mnf 8152 df-ltxr 8154 df-inn 9079 df-2 9137 df-3 9138 df-ndx 13001 df-slot 13002 df-base 13004 df-sets 13005 df-plusg 13089 df-mulr 13090 df-0g 13257 df-mgm 13355 df-sgrp 13401 df-mnd 13416 df-mhm 13458 df-grp 13502 df-ghm 13744 df-mgp 13850 df-ur 13889 df-ring 13927 df-rhm 14081

This theorem is referenced by: zrhpropd 14555

W3C validator