Theorem rhmpreimacnlem

Description: Lemma for rhmpreimacn . (Contributed by Thierry Arnoux, 7-Jul-2024)

	Ref	Expression
Hypotheses	rhmpreimacn.t	⊢ 𝑇 = ( Spec ‘ 𝑅 )
	rhmpreimacn.u	⊢ 𝑈 = ( Spec ‘ 𝑆 )
	rhmpreimacn.a	⊢ 𝐴 = ( PrmIdeal ‘ 𝑅 )
	rhmpreimacn.b	⊢ 𝐵 = ( PrmIdeal ‘ 𝑆 )
	rhmpreimacn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑇 )
	rhmpreimacn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑈 )
	rhmpreimacn.g	⊢ 𝐺 = ( 𝑖 ∈ 𝐵 ↦ ( ◡ 𝐹 “ 𝑖 ) )
	rhmpreimacn.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	rhmpreimacn.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	rhmpreimacn.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
	rhmpreimacn.1	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑆 ) )
	rhmpreimacnlem.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	rhmpreimacnlem.v	⊢ 𝑉 = ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } )
	rhmpreimacnlem.w	⊢ 𝑊 = ( 𝑗 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } )
Assertion	rhmpreimacnlem	⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) = ( ◡ 𝐺 “ ( 𝑉 ‘ 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmpreimacn.t	⊢ 𝑇 = ( Spec ‘ 𝑅 )
2		rhmpreimacn.u	⊢ 𝑈 = ( Spec ‘ 𝑆 )
3		rhmpreimacn.a	⊢ 𝐴 = ( PrmIdeal ‘ 𝑅 )
4		rhmpreimacn.b	⊢ 𝐵 = ( PrmIdeal ‘ 𝑆 )
5		rhmpreimacn.j	⊢ 𝐽 = ( TopOpen ‘ 𝑇 )
6		rhmpreimacn.k	⊢ 𝐾 = ( TopOpen ‘ 𝑈 )
7		rhmpreimacn.g	⊢ 𝐺 = ( 𝑖 ∈ 𝐵 ↦ ( ◡ 𝐹 “ 𝑖 ) )
8		rhmpreimacn.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
9		rhmpreimacn.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
10		rhmpreimacn.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
11		rhmpreimacn.1	⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝑆 ) )
12		rhmpreimacnlem.1	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
13		rhmpreimacnlem.v	⊢ 𝑉 = ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } )
14		rhmpreimacnlem.w	⊢ 𝑊 = ( 𝑗 ∈ ( LIdeal ‘ 𝑆 ) ↦ { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } )
15		imaeq2	⊢ ( 𝑖 = 𝑔 → ( ◡ 𝐹 “ 𝑖 ) = ( ◡ 𝐹 “ 𝑔 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
17	10	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
18		cnvexg	⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
19		imaexg	⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ 𝑔 ) ∈ V )
20	17 18 19	3syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑔 ) ∈ V )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑔 ) ∈ V )
22	7 15 16 21	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑔 ) = ( ◡ 𝐹 “ 𝑔 ) )
23	22	eleq1d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ↔ ( ◡ 𝐹 “ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) )
24	23	pm5.32da	⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ) )
25	9	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑆 ∈ CRing )
26	10	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ 𝐵 )
28	27 4	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑆 ) )
29	3	rhmpreimaprmidl	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝑖 ) ∈ 𝐴 )
30	25 26 28 29	syl21anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑖 ) ∈ 𝐴 )
31	30 7	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
32	31	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
33		elpreima	⊢ ( 𝐺 Fn 𝐵 → ( 𝑔 ∈ ( ◡ 𝐺 “ ( 𝑉 ‘ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ) )
34	32 33	syl	⊢ ( 𝜑 → ( 𝑔 ∈ ( ◡ 𝐺 “ ( 𝑉 ‘ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ) )
35		sseq1	⊢ ( 𝑗 = ( 𝐹 “ 𝐼 ) → ( 𝑗 ⊆ 𝑘 ↔ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 ) )
36	35	rabbidv	⊢ ( 𝑗 = ( 𝐹 “ 𝐼 ) → { 𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘 } = { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } )
37		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
38		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
39		eqid	⊢ ( LIdeal ‘ 𝑆 ) = ( LIdeal ‘ 𝑆 )
40	37 38 39	rhmimaidl	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ran 𝐹 = ( Base ‘ 𝑆 ) ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝐹 “ 𝐼 ) ∈ ( LIdeal ‘ 𝑆 ) )
41	10 11 12 40	syl3anc	⊢ ( 𝜑 → ( 𝐹 “ 𝐼 ) ∈ ( LIdeal ‘ 𝑆 ) )
42	4	fvexi	⊢ 𝐵 ∈ V
43	42	rabex	⊢ { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } ∈ V
44	43	a1i	⊢ ( 𝜑 → { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } ∈ V )
45	14 36 41 44	fvmptd3	⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) = { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } )
46	45	eleq2d	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ 𝑔 ∈ { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } ) )
47		sseq2	⊢ ( 𝑘 = 𝑔 → ( ( 𝐹 “ 𝐼 ) ⊆ 𝑘 ↔ ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ) )
48	47	elrab	⊢ ( 𝑔 ∈ { 𝑘 ∈ 𝐵 ∣ ( 𝐹 “ 𝐼 ) ⊆ 𝑘 } ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ) )
49	46 48	bitrdi	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ) ) )
50		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
51	50 37	rhmf	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
52	10 51	syl	⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
53	52	ffund	⊢ ( 𝜑 → Fun 𝐹 )
54	50 38	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
55	12 54	syl	⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
56	52	fdmd	⊢ ( 𝜑 → dom 𝐹 = ( Base ‘ 𝑅 ) )
57	55 56	sseqtrrd	⊢ ( 𝜑 → 𝐼 ⊆ dom 𝐹 )
58		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝐼 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ↔ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) )
59	53 57 58	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ↔ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) )
60	59	anbi2d	⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐵 ∧ ( 𝐹 “ 𝐼 ) ⊆ 𝑔 ) ↔ ( 𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ) )
61	9	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑆 ∈ CRing )
62	10	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
63	16 4	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( PrmIdeal ‘ 𝑆 ) )
64	3	rhmpreimaprmidl	⊢ ( ( ( 𝑆 ∈ CRing ∧ 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ 𝑔 ∈ ( PrmIdeal ‘ 𝑆 ) ) → ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 )
65	61 62 63 64	syl21anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 )
66	65	biantrurd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ↔ ( ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ) )
67	66	pm5.32da	⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐵 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ) ) )
68	49 60 67	3bitrd	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ) ) )
69		sseq2	⊢ ( 𝑘 = ( ◡ 𝐹 “ 𝑔 ) → ( 𝐼 ⊆ 𝑘 ↔ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) )
70	69	elrab	⊢ ( ( ◡ 𝐹 “ 𝑔 ) ∈ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ↔ ( ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) )
71	70	anbi2i	⊢ ( ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ( ◡ 𝐹 “ 𝑔 ) ∈ 𝐴 ∧ 𝐼 ⊆ ( ◡ 𝐹 “ 𝑔 ) ) ) )
72	68 71	bitr4di	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ) ) )
73		sseq1	⊢ ( 𝑗 = 𝐼 → ( 𝑗 ⊆ 𝑘 ↔ 𝐼 ⊆ 𝑘 ) )
74	73	rabbidv	⊢ ( 𝑗 = 𝐼 → { 𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘 } = { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } )
75	3	fvexi	⊢ 𝐴 ∈ V
76	75	rabex	⊢ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ∈ V
77	76	a1i	⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ∈ V )
78	13 74 12 77	fvmptd3	⊢ ( 𝜑 → ( 𝑉 ‘ 𝐼 ) = { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } )
79	78	eleq2d	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ↔ ( ◡ 𝐹 “ 𝑔 ) ∈ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ) )
80	79	anbi2d	⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ { 𝑘 ∈ 𝐴 ∣ 𝐼 ⊆ 𝑘 } ) ) )
81	72 80	bitr4d	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ( 𝑔 ∈ 𝐵 ∧ ( ◡ 𝐹 “ 𝑔 ) ∈ ( 𝑉 ‘ 𝐼 ) ) ) )
82	24 34 81	3bitr4rd	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) ↔ 𝑔 ∈ ( ◡ 𝐺 “ ( 𝑉 ‘ 𝐼 ) ) ) )
83	82	eqrdv	⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐹 “ 𝐼 ) ) = ( ◡ 𝐺 “ ( 𝑉 ‘ 𝐼 ) ) )