rhmsubcALTVlem3

Description: Lemma 3 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
	rngcrescrhmALTV.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion	rhmsubcALTVlem3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
3		rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4		rngcrescrhmALTV.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5	3	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 ↔ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) )
6		elinel1	⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ Ring )
7	5 6	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 → 𝑥 ∈ Ring ) )
8	7	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ Ring )
9		eqid	⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
10	9	idrhm	⊢ ( 𝑥 ∈ Ring → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
11	8 10	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
12	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑈 ∈ 𝑉 )
13		eqid	⊢ ( RngCatALTV ‘ 𝑈 ) = ( RngCatALTV ‘ 𝑈 )
14		eqid	⊢ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( Base ‘ ( RngCatALTV ‘ 𝑈 ) )
15	13 14	rngccatidALTV	⊢ ( 𝑈 ∈ 𝑉 → ( ( RngCatALTV ‘ 𝑈 ) ∈ Cat ∧ ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ↦ ( I ↾ ( Base ‘ 𝑦 ) ) ) ) )
16		simpr	⊢ ( ( ( RngCatALTV ‘ 𝑈 ) ∈ Cat ∧ ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ↦ ( I ↾ ( Base ‘ 𝑦 ) ) ) ) → ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ↦ ( I ↾ ( Base ‘ 𝑦 ) ) ) )
17	12 15 16	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑦 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) ↦ ( I ↾ ( Base ‘ 𝑦 ) ) ) )
18		fveq2	⊢ ( 𝑦 = 𝑥 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑥 ) )
19	18	reseq2d	⊢ ( 𝑦 = 𝑥 → ( I ↾ ( Base ‘ 𝑦 ) ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑦 = 𝑥 ) → ( I ↾ ( Base ‘ 𝑦 ) ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
21		incom	⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
22	3 21	eqtrdi	⊢ ( 𝜑 → 𝑅 = ( 𝑈 ∩ Ring ) )
23	22	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 ↔ 𝑥 ∈ ( 𝑈 ∩ Ring ) ) )
24		ringrng	⊢ ( 𝑥 ∈ Ring → 𝑥 ∈ Rng )
25	24	anim2i	⊢ ( ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Ring ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
26		elin	⊢ ( 𝑥 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Ring ) )
27		elin	⊢ ( 𝑥 ∈ ( 𝑈 ∩ Rng ) ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
28	25 26 27	3imtr4i	⊢ ( 𝑥 ∈ ( 𝑈 ∩ Ring ) → 𝑥 ∈ ( 𝑈 ∩ Rng ) )
29	23 28	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 → 𝑥 ∈ ( 𝑈 ∩ Rng ) ) )
30	29	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ ( 𝑈 ∩ Rng ) )
31	2	eqcomi	⊢ ( RngCatALTV ‘ 𝑈 ) = 𝐶
32	31	fveq2i	⊢ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( Base ‘ 𝐶 )
33	2 32 1	rngcbasALTV	⊢ ( 𝜑 → ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑈 ∩ Rng ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) = ( 𝑈 ∩ Rng ) )
35	30 34	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ ( Base ‘ ( RngCatALTV ‘ 𝑈 ) ) )
36		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( Base ‘ 𝑥 ) ∈ V )
37	36	resiexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ V )
38	17 20 35 37	fvmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
39	1 2 3 4	rhmsubcALTVlem2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
40	39	3anidm23	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
41	11 38 40	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCatALTV ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Metamath Proof Explorer

Theorem rhmsubcALTVlem3

Proof