issubrg2 - Intuitionistic Logic Explorer

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

Theorem issubrg2 14003

Description: Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.)

**Hypotheses**
Ref	Expression
issubrg2.b	⊢ 𝐵 = (Base‘𝑅)
issubrg2.o	⊢ 1 = (1_r‘𝑅)
issubrg2.t	⊢ · = (._r‘𝑅)

**Assertion**
Ref	Expression
issubrg2	⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝑅,𝑦 𝑥, · ,𝑦 Allowed substitution hints: 𝐵(𝑥,𝑦) 1 (𝑥,𝑦)

Proof of Theorem issubrg2 Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		subrgsubg 13989	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
2		issubrg2.o	. . . 4 ⊢ 1 = (1_r‘𝑅)
3	2	subrg1cl 13991	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
4		issubrg2.t	. . . . . 6 ⊢ · = (._r‘𝑅)
5	4	subrgmcl 13995	. . . . 5 ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)
6	5	3expb 1207	. . . 4 ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 · 𝑦) ∈ 𝐴)
7	6	ralrimivva 2588	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)
8	1, 3, 7	3jca 1180	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴))
9		simpl 109	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝑅 ∈ Ring)
10		simpr1 1006	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 ∈ (SubGrp‘𝑅))
11		eqid 2205	. . . . . . 7 ⊢ (𝑅 ↾_s 𝐴) = (𝑅 ↾_s 𝐴)
12	11	subgbas 13514	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 = (Base‘(𝑅 ↾_s 𝐴)))
13	10, 12	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 = (Base‘(𝑅 ↾_s 𝐴)))
14		eqidd 2206	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (𝑅 ↾_s 𝐴) = (𝑅 ↾_s 𝐴))
15		eqidd 2206	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (+_g‘𝑅) = (+_g‘𝑅))
16		id 19	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
17		subgrcl 13515	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝑅 ∈ Grp)
18	14, 15, 16, 17	ressplusgd 12961	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (+_g‘𝑅) = (+_g‘(𝑅 ↾_s 𝐴)))
19	10, 18	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (+_g‘𝑅) = (+_g‘(𝑅 ↾_s 𝐴)))
20	11, 4	ressmulrg 12977	. . . . . 6 ⊢ ((𝐴 ∈ (SubGrp‘𝑅) ∧ 𝑅 ∈ Grp) → · = (._r‘(𝑅 ↾_s 𝐴)))
21	10, 17, 20	syl2anc2 412	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → · = (._r‘(𝑅 ↾_s 𝐴)))
22	11	subggrp 13513	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (𝑅 ↾_s 𝐴) ∈ Grp)
23	10, 22	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑅 ↾_s 𝐴) ∈ Grp)
24		simpr3 1008	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)
25		oveq1 5951	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑥 · 𝑦) = (𝑢 · 𝑦))
26	25	eleq1d 2274	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((𝑥 · 𝑦) ∈ 𝐴 ↔ (𝑢 · 𝑦) ∈ 𝐴))
27		oveq2 5952	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → (𝑢 · 𝑦) = (𝑢 · 𝑣))
28	27	eleq1d 2274	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → ((𝑢 · 𝑦) ∈ 𝐴 ↔ (𝑢 · 𝑣) ∈ 𝐴))
29	26, 28	rspc2v 2890	. . . . . . 7 ⊢ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴 → (𝑢 · 𝑣) ∈ 𝐴))
30	24, 29	syl5com 29	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 · 𝑣) ∈ 𝐴))
31	30	3impib 1204	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑢 · 𝑣) ∈ 𝐴)
32		issubrg2.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑅)
33	32	subgss 13510	. . . . . . . . . 10 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 ⊆ 𝐵)
34	10, 33	syl 14	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 ⊆ 𝐵)
35	34	sseld 3192	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵))
36	34	sseld 3192	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑣 ∈ 𝐴 → 𝑣 ∈ 𝐵))
37	34	sseld 3192	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵))
38	35, 36, 37	3anim123d 1332	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))
39	38	imp 124	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))
40	32, 4	ringass 13778	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
41	40	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
42	39, 41	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
43		eqid 2205	. . . . . . . 8 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
44	32, 43, 4	ringdi 13780	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢 · (𝑣(+_g‘𝑅)𝑤)) = ((𝑢 · 𝑣)(+_g‘𝑅)(𝑢 · 𝑤)))
45	44	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑢 · (𝑣(+_g‘𝑅)𝑤)) = ((𝑢 · 𝑣)(+_g‘𝑅)(𝑢 · 𝑤)))
46	39, 45	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝑢 · (𝑣(+_g‘𝑅)𝑤)) = ((𝑢 · 𝑣)(+_g‘𝑅)(𝑢 · 𝑤)))
47	32, 43, 4	ringdir 13781	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑅)𝑣) · 𝑤) = ((𝑢 · 𝑤)(+_g‘𝑅)(𝑣 · 𝑤)))
48	47	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+_g‘𝑅)𝑣) · 𝑤) = ((𝑢 · 𝑤)(+_g‘𝑅)(𝑣 · 𝑤)))
49	39, 48	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑢(+_g‘𝑅)𝑣) · 𝑤) = ((𝑢 · 𝑤)(+_g‘𝑅)(𝑣 · 𝑤)))
50		simpr2 1007	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 1 ∈ 𝐴)
51	35	imp 124	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐴) → 𝑢 ∈ 𝐵)
52	32, 4, 2	ringlidm 13785	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵) → ( 1 · 𝑢) = 𝑢)
53	52	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐵) → ( 1 · 𝑢) = 𝑢)
54	51, 53	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐴) → ( 1 · 𝑢) = 𝑢)
55	32, 4, 2	ringridm 13786	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵) → (𝑢 · 1 ) = 𝑢)
56	55	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐵) → (𝑢 · 1 ) = 𝑢)
57	51, 56	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ 𝑢 ∈ 𝐴) → (𝑢 · 1 ) = 𝑢)
58	13, 19, 21, 23, 31, 42, 46, 49, 50, 54, 57	isringd 13803	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑅 ↾_s 𝐴) ∈ Ring)
59	34, 50	jca 306	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))
60	32, 2	issubrg 13983	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) ↔ ((𝑅 ∈ Ring ∧ (𝑅 ↾_s 𝐴) ∈ Ring) ∧ (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴)))
61	9, 58, 59, 60	syl21anbrc 1185	. . 3 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 ∈ (SubRing‘𝑅))
62	61	ex 115	. 2 ⊢ (𝑅 ∈ Ring → ((𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴) → 𝐴 ∈ (SubRing‘𝑅)))
63	8, 62	impbid2 143	1 ⊢ (𝑅 ∈ Ring → (𝐴 ∈ (SubRing‘𝑅) ↔ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 981 = wceq 1373 ∈ wcel 2176 ∀wral 2484 ⊆ wss 3166 ‘cfv 5271 (class class class)co 5944 Basecbs 12832 ↾_s cress 12833 +_gcplusg 12909 ._rcmulr 12910 Grpcgrp 13332 SubGrpcsubg 13503 1_rcur 13721 Ringcrg 13758 SubRingcsubrg 13979

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-cnex 8016 ax-resscn 8017 ax-1cn 8018 ax-1re 8019 ax-icn 8020 ax-addcl 8021 ax-addrcl 8022 ax-mulcl 8023 ax-addcom 8025 ax-addass 8027 ax-i2m1 8030 ax-0lt1 8031 ax-0id 8033 ax-rnegex 8034 ax-pre-ltirr 8037 ax-pre-lttrn 8039 ax-pre-ltadd 8041

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-br 4045 df-opab 4106 df-mpt 4107 df-id 4340 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-fv 5279 df-riota 5899 df-ov 5947 df-oprab 5948 df-mpo 5949 df-pnf 8109 df-mnf 8110 df-ltxr 8112 df-inn 9037 df-2 9095 df-3 9096 df-ndx 12835 df-slot 12836 df-base 12838 df-sets 12839 df-iress 12840 df-plusg 12922 df-mulr 12923 df-0g 13090 df-mgm 13188 df-sgrp 13234 df-mnd 13249 df-subg 13506 df-mgp 13683 df-ur 13722 df-ring 13760 df-subrg 13981

This theorem is referenced by: subrgintm 14005 issubrg3 14009 issubrgd 14214 cnsubrglem 14342

W3C validator