Theorem rhmpreimaidl 21273

Description: The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)

Hypothesis

Ref	Expression
rhmpreimaidl.i	⊢ 𝐼 = (LIdeal‘𝑅)

Assertion

Ref	Expression
rhmpreimaidl	⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝐼)

Proof of Theorem rhmpreimaidl

Dummy variables 𝑎 𝑏 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvimass 6045	. . . 4 ⊢ (◡𝐹 “ 𝐽) ⊆ dom 𝐹
2		eqid 2737	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		eqid 2737	. . . . 5 ⊢ (Base‘𝑆) = (Base‘𝑆)
4	2, 3	rhmf 20461	. . . 4 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
5	1, 4	fssdm 6685	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (◡𝐹 “ 𝐽) ⊆ (Base‘𝑅))
6	5	adantr 480	. 2 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ⊆ (Base‘𝑅))
7	4	adantr 480	. . . . 5 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → 𝐹:(Base‘𝑅)⟶(Base‘𝑆))
8	7	ffund 6670	. . . 4 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → Fun 𝐹)
9		rhmrcl1 20453	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring)
10	9	adantr 480	. . . . . 6 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → 𝑅 ∈ Ring)
11		eqid 2737	. . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅)
12	2, 11	ring0cl 20245	. . . . . 6 ⊢ (𝑅 ∈ Ring → (0g‘𝑅) ∈ (Base‘𝑅))
13	10, 12	syl 17	. . . . 5 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (0g‘𝑅) ∈ (Base‘𝑅))
14	7	fdmd 6676	. . . . 5 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → dom 𝐹 = (Base‘𝑅))
15	13, 14	eleqtrrd 2840	. . . 4 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (0g‘𝑅) ∈ dom 𝐹)
16		rhmghm 20460	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
17		ghmmhm 19198	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹 ∈ (𝑅 MndHom 𝑆))
18		eqid 2737	. . . . . . . 8 ⊢ (0g‘𝑆) = (0g‘𝑆)
19	11, 18	mhm0 18759	. . . . . . 7 ⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆))
20	16, 17, 19	3syl 18	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆))
21	20	adantr 480	. . . . 5 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆))
22		rhmrcl2 20454	. . . . . 6 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝑆 ∈ Ring)
23		eqid 2737	. . . . . . 7 ⊢ (LIdeal‘𝑆) = (LIdeal‘𝑆)
24	23, 18	lidl0cl 21216	. . . . . 6 ⊢ ((𝑆 ∈ Ring ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (0g‘𝑆) ∈ 𝐽)
25	22, 24	sylan 581	. . . . 5 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (0g‘𝑆) ∈ 𝐽)
26	21, 25	eqeltrd 2837	. . . 4 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (𝐹‘(0g‘𝑅)) ∈ 𝐽)
27		fvimacnv 7003	. . . . 5 ⊢ ((Fun 𝐹 ∧ (0g‘𝑅) ∈ dom 𝐹) → ((𝐹‘(0g‘𝑅)) ∈ 𝐽 ↔ (0g‘𝑅) ∈ (◡𝐹 “ 𝐽)))
28	27	biimpa 476	. . . 4 ⊢ (((Fun 𝐹 ∧ (0g‘𝑅) ∈ dom 𝐹) ∧ (𝐹‘(0g‘𝑅)) ∈ 𝐽) → (0g‘𝑅) ∈ (◡𝐹 “ 𝐽))
29	8, 15, 26, 28	syl21anc 838	. . 3 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (0g‘𝑅) ∈ (◡𝐹 “ 𝐽))
30	29	ne0d 4283	. 2 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ≠ ∅)
31	7	ffnd 6667	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → 𝐹 Fn (Base‘𝑅))
32	31	ad3antrrr 731	. . . . . 6 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝐹 Fn (Base‘𝑅))
33	10	ad3antrrr 731	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑅 ∈ Ring)
34		simpllr 776	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑥 ∈ (Base‘𝑅))
35	5	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → (◡𝐹 “ 𝐽) ⊆ (Base‘𝑅))
36	35	sselda 3922	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) → 𝑎 ∈ (Base‘𝑅))
37	36	adantr 480	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑎 ∈ (Base‘𝑅))
38		eqid 2737	. . . . . . . . 9 ⊢ (.r‘𝑅) = (.r‘𝑅)
39	2, 38	ringcl 20228	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑎) ∈ (Base‘𝑅))
40	33, 34, 37, 39	syl3anc 1374	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝑥(.r‘𝑅)𝑎) ∈ (Base‘𝑅))
41	35	adantr 480	. . . . . . . 8 ⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) → (◡𝐹 “ 𝐽) ⊆ (Base‘𝑅))
42	41	sselda 3922	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑏 ∈ (Base‘𝑅))
43		eqid 2737	. . . . . . . 8 ⊢ (+g‘𝑅) = (+g‘𝑅)
44	2, 43	ringacl 20256	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑥(.r‘𝑅)𝑎) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (Base‘𝑅))
45	33, 40, 42, 44	syl3anc 1374	. . . . . 6 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (Base‘𝑅))
46	16	ad4antr 733	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
47		eqid 2737	. . . . . . . . 9 ⊢ (+g‘𝑆) = (+g‘𝑆)
48	2, 43, 47	ghmlin 19193	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥(.r‘𝑅)𝑎) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → (𝐹‘((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏)) = ((𝐹‘(𝑥(.r‘𝑅)𝑎))(+g‘𝑆)(𝐹‘𝑏)))
49	46, 40, 42, 48	syl3anc 1374	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏)) = ((𝐹‘(𝑥(.r‘𝑅)𝑎))(+g‘𝑆)(𝐹‘𝑏)))
50		simp-4l 783	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
51	50, 22	syl 17	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑆 ∈ Ring)
52		simpr 484	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → 𝐽 ∈ (LIdeal‘𝑆))
53	52	ad3antrrr 731	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝐽 ∈ (LIdeal‘𝑆))
54		eqid 2737	. . . . . . . . . . 11 ⊢ (.r‘𝑆) = (.r‘𝑆)
55	2, 38, 54	rhmmul 20462	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ (Base‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑎)) = ((𝐹‘𝑥)(.r‘𝑆)(𝐹‘𝑎)))
56	50, 34, 37, 55	syl3anc 1374	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘(𝑥(.r‘𝑅)𝑎)) = ((𝐹‘𝑥)(.r‘𝑆)(𝐹‘𝑎)))
57	7	ffvelcdmda 7034	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ (Base‘𝑆))
58	57	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘𝑥) ∈ (Base‘𝑆))
59		simplr 769	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑎 ∈ (◡𝐹 “ 𝐽))
60		elpreima 7008	. . . . . . . . . . . 12 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑎 ∈ (◡𝐹 “ 𝐽) ↔ (𝑎 ∈ (Base‘𝑅) ∧ (𝐹‘𝑎) ∈ 𝐽)))
61	60	simplbda 499	. . . . . . . . . . 11 ⊢ ((𝐹 Fn (Base‘𝑅) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘𝑎) ∈ 𝐽)
62	32, 59, 61	syl2anc 585	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘𝑎) ∈ 𝐽)
63	23, 3, 54	lidlmcl 21221	. . . . . . . . . 10 ⊢ (((𝑆 ∈ Ring ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ ((𝐹‘𝑥) ∈ (Base‘𝑆) ∧ (𝐹‘𝑎) ∈ 𝐽)) → ((𝐹‘𝑥)(.r‘𝑆)(𝐹‘𝑎)) ∈ 𝐽)
64	51, 53, 58, 62, 63	syl22anc 839	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → ((𝐹‘𝑥)(.r‘𝑆)(𝐹‘𝑎)) ∈ 𝐽)
65	56, 64	eqeltrd 2837	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘(𝑥(.r‘𝑅)𝑎)) ∈ 𝐽)
66		simpr 484	. . . . . . . . 9 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → 𝑏 ∈ (◡𝐹 “ 𝐽))
67		elpreima 7008	. . . . . . . . . 10 ⊢ (𝐹 Fn (Base‘𝑅) → (𝑏 ∈ (◡𝐹 “ 𝐽) ↔ (𝑏 ∈ (Base‘𝑅) ∧ (𝐹‘𝑏) ∈ 𝐽)))
68	67	simplbda 499	. . . . . . . . 9 ⊢ ((𝐹 Fn (Base‘𝑅) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘𝑏) ∈ 𝐽)
69	32, 66, 68	syl2anc 585	. . . . . . . 8 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘𝑏) ∈ 𝐽)
70	23, 47	lidlacl 21217	. . . . . . . 8 ⊢ (((𝑆 ∈ Ring ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ ((𝐹‘(𝑥(.r‘𝑅)𝑎)) ∈ 𝐽 ∧ (𝐹‘𝑏) ∈ 𝐽)) → ((𝐹‘(𝑥(.r‘𝑅)𝑎))(+g‘𝑆)(𝐹‘𝑏)) ∈ 𝐽)
71	51, 53, 65, 69, 70	syl22anc 839	. . . . . . 7 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → ((𝐹‘(𝑥(.r‘𝑅)𝑎))(+g‘𝑆)(𝐹‘𝑏)) ∈ 𝐽)
72	49, 71	eqeltrd 2837	. . . . . 6 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → (𝐹‘((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏)) ∈ 𝐽)
73	32, 45, 72	elpreimad 7009	. . . . 5 ⊢ (((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ (◡𝐹 “ 𝐽)) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (◡𝐹 “ 𝐽))
74	73	anasss 466	. . . 4 ⊢ ((((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑎 ∈ (◡𝐹 “ 𝐽) ∧ 𝑏 ∈ (◡𝐹 “ 𝐽))) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (◡𝐹 “ 𝐽))
75	74	ralrimivva 3181	. . 3 ⊢ (((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∀𝑎 ∈ (◡𝐹 “ 𝐽)∀𝑏 ∈ (◡𝐹 “ 𝐽)((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (◡𝐹 “ 𝐽))
76	75	ralrimiva 3130	. 2 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∀𝑎 ∈ (◡𝐹 “ 𝐽)∀𝑏 ∈ (◡𝐹 “ 𝐽)((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (◡𝐹 “ 𝐽))
77		rhmpreimaidl.i	. . 3 ⊢ 𝐼 = (LIdeal‘𝑅)
78	77, 2, 43, 38	islidl 21211	. 2 ⊢ ((◡𝐹 “ 𝐽) ∈ 𝐼 ↔ ((◡𝐹 “ 𝐽) ⊆ (Base‘𝑅) ∧ (◡𝐹 “ 𝐽) ≠ ∅ ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑎 ∈ (◡𝐹 “ 𝐽)∀𝑏 ∈ (◡𝐹 “ 𝐽)((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (◡𝐹 “ 𝐽)))
79	6, 30, 76, 78	syl3anbrc 1345	1 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝐼)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052   ⊆ wss 3890  ∅c0 4274  ^◡ccnv 5627  dom cdm 5628   “ cima 5631  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7364  Basecbs 17176  +_gcplusg 17217  ._rcmulr 17218  0_gc0g 17399   MndHom cmhm 18746   GrpHom cghm 19184  Ringcrg 20211   RingHom crh 20446  LIdealclidl 21202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-om 7815  df-1st 7939  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-nn 12172  df-2 12241  df-3 12242  df-4 12243  df-5 12244  df-6 12245  df-7 12246  df-8 12247  df-sets 17131  df-slot 17149  df-ndx 17161  df-base 17177  df-ress 17198  df-plusg 17230  df-mulr 17231  df-sca 17233  df-vsca 17234  df-ip 17235  df-0g 17401  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-mhm 18748  df-grp 18909  df-minusg 18910  df-sbg 18911  df-subg 19096  df-ghm 19185  df-cmn 19754  df-abl 19755  df-mgp 20119  df-rng 20131  df-ur 20160  df-ring 20213  df-rhm 20449  df-subrg 20544  df-lmod 20854  df-lss 20924  df-sra 21166  df-rgmod 21167  df-lidl 21204

This theorem is referenced by:  kerlidl  21274  rhmpreimaprmidl  33532  ply1annidl  33868