issubrg2 - Intuitionistic Logic Explorer

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

Theorem issubrg2 14088

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 14074	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
2		issubrg2.o	. . . 4 ⊢ 1 = (1_r‘𝑅)
3	2	subrg1cl 14076	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 1 ∈ 𝐴)
4		issubrg2.t	. . . . . 6 ⊢ · = (._r‘𝑅)
5	4	subrgmcl 14080	. . . . 5 ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 · 𝑦) ∈ 𝐴)
6	5	3expb 1207	. . . 4 ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 · 𝑦) ∈ 𝐴)
7	6	ralrimivva 2589	. . 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 2206	. . . . . . 7 ⊢ (𝑅 ↾_s 𝐴) = (𝑅 ↾_s 𝐴)
12	11	subgbas 13599	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 = (Base‘(𝑅 ↾_s 𝐴)))
13	10, 12	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 = (Base‘(𝑅 ↾_s 𝐴)))
14		eqidd 2207	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (𝑅 ↾_s 𝐴) = (𝑅 ↾_s 𝐴))
15		eqidd 2207	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (+_g‘𝑅) = (+_g‘𝑅))
16		id 19	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅))
17		subgrcl 13600	. . . . . . 7 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝑅 ∈ Grp)
18	14, 15, 16, 17	ressplusgd 13046	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (+_g‘𝑅) = (+_g‘(𝑅 ↾_s 𝐴)))
19	10, 18	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (+_g‘𝑅) = (+_g‘(𝑅 ↾_s 𝐴)))
20	11, 4	ressmulrg 13062	. . . . . 6 ⊢ ((𝐴 ∈ (SubGrp‘𝑅) ∧ 𝑅 ∈ Grp) → · = (._r‘(𝑅 ↾_s 𝐴)))
21	10, 17, 20	syl2anc2 412	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → · = (._r‘(𝑅 ↾_s 𝐴)))
22	11	subggrp 13598	. . . . . 6 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → (𝑅 ↾_s 𝐴) ∈ Grp)
23	10, 22	syl 14	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑅 ↾_s 𝐴) ∈ Grp)
24		simpr3 1008	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)
25		oveq1 5969	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (𝑥 · 𝑦) = (𝑢 · 𝑦))
26	25	eleq1d 2275	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → ((𝑥 · 𝑦) ∈ 𝐴 ↔ (𝑢 · 𝑦) ∈ 𝐴))
27		oveq2 5970	. . . . . . . . 9 ⊢ (𝑦 = 𝑣 → (𝑢 · 𝑦) = (𝑢 · 𝑣))
28	27	eleq1d 2275	. . . . . . . 8 ⊢ (𝑦 = 𝑣 → ((𝑢 · 𝑦) ∈ 𝐴 ↔ (𝑢 · 𝑣) ∈ 𝐴))
29	26, 28	rspc2v 2894	. . . . . . 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 13595	. . . . . . . . . 10 ⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 ⊆ 𝐵)
34	10, 33	syl 14	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → 𝐴 ⊆ 𝐵)
35	34	sseld 3196	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵))
36	34	sseld 3196	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑣 ∈ 𝐴 → 𝑣 ∈ 𝐵))
37	34	sseld 3196	. . . . . . . 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 13863	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
41	40	adantlr 477	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
42	39, 41	syldan 282	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑢 · 𝑣) · 𝑤) = (𝑢 · (𝑣 · 𝑤)))
43		eqid 2206	. . . . . . . 8 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
44	32, 43, 4	ringdi 13865	. . . . . . 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 13866	. . . . . . 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 13870	. . . . . . 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 13871	. . . . . . 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 13888	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝑅 ↾_s 𝐴) ∈ Ring)
59	34, 50	jca 306	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ (SubGrp‘𝑅) ∧ 1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 · 𝑦) ∈ 𝐴)) → (𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴))
60	32, 2	issubrg 14068	. . . 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 2177 ∀wral 2485 ⊆ wss 3170 ‘cfv 5285 (class class class)co 5962 Basecbs 12917 ↾_s cress 12918 +_gcplusg 12994 ._rcmulr 12995 Grpcgrp 13417 SubGrpcsubg 13588 1_rcur 13806 Ringcrg 13843 SubRingcsubrg 14064

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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4173 ax-pow 4229 ax-pr 4264 ax-un 4493 ax-setind 4598 ax-cnex 8046 ax-resscn 8047 ax-1cn 8048 ax-1re 8049 ax-icn 8050 ax-addcl 8051 ax-addrcl 8052 ax-mulcl 8053 ax-addcom 8055 ax-addass 8057 ax-i2m1 8060 ax-0lt1 8061 ax-0id 8063 ax-rnegex 8064 ax-pre-ltirr 8067 ax-pre-lttrn 8069 ax-pre-ltadd 8071

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3860 df-int 3895 df-br 4055 df-opab 4117 df-mpt 4118 df-id 4353 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-ima 4701 df-iota 5246 df-fun 5287 df-fn 5288 df-fv 5293 df-riota 5917 df-ov 5965 df-oprab 5966 df-mpo 5967 df-pnf 8139 df-mnf 8140 df-ltxr 8142 df-inn 9067 df-2 9125 df-3 9126 df-ndx 12920 df-slot 12921 df-base 12923 df-sets 12924 df-iress 12925 df-plusg 13007 df-mulr 13008 df-0g 13175 df-mgm 13273 df-sgrp 13319 df-mnd 13334 df-subg 13591 df-mgp 13768 df-ur 13807 df-ring 13845 df-subrg 14066

This theorem is referenced by: subrgintm 14090 issubrg3 14094 issubrgd 14299 cnsubrglem 14427

W3C validator