Theorem rhmsubcrngclem1

Description: Lemma 1 for rhmsubcrngc . (Contributed by AV, 9-Mar-2020)

	Ref	Expression
Hypotheses	rhmsubcrngc.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	rhmsubcrngc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rhmsubcrngc.b	⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
	rhmsubcrngc.h	⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion	rhmsubcrngclem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmsubcrngc.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2		rhmsubcrngc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		rhmsubcrngc.b	⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
4		rhmsubcrngc.h	⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5	3	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) )
6		elin	⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) ↔ ( 𝑥 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) )
7	6	simplbi	⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ Ring )
8	5 7	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ Ring ) )
9	8	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ Ring )
10		eqid	⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
11	10	idrhm	⊢ ( 𝑥 ∈ Ring → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
12	9 11	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
15	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ 𝑉 )
16		ringrng	⊢ ( 𝑥 ∈ Ring → 𝑥 ∈ Rng )
17	16	anim2i	⊢ ( ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Ring ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
18	17	ancoms	⊢ ( ( 𝑥 ∈ Ring ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
19	6 18	sylbi	⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) → ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
21		elin	⊢ ( 𝑥 ∈ ( 𝑈 ∩ Rng ) ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
22	20 21	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) → 𝑥 ∈ ( 𝑈 ∩ Rng ) )
23	1 13 2	rngcbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
25	22 24	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
26	25	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
27	5 26	sylbid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
28	27	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
29	1 13 14 15 28 10	rngcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
30	4	oveqdr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
31		eqid	⊢ ( RingCat ‘ 𝑈 ) = ( RingCat ‘ 𝑈 )
32		eqid	⊢ ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( Base ‘ ( RingCat ‘ 𝑈 ) )
33		eqid	⊢ ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( Hom ‘ ( RingCat ‘ 𝑈 ) )
34	31 32 2 33	ringchomfval	⊢ ( 𝜑 → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) ) )
35	31 32 2	ringcbas	⊢ ( 𝜑 → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
36		incom	⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
37	3 36	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
38	37	eqcomd	⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) = 𝐵 )
39	35 38	eqtrd	⊢ ( 𝜑 → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = 𝐵 )
40	39	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) = ( 𝐵 × 𝐵 ) )
41	40	reseq2d	⊢ ( 𝜑 → ( RingHom ↾ ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
42	34 41	eqtrd	⊢ ( 𝜑 → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
44	43	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) = ( Hom ‘ ( RingCat ‘ 𝑈 ) ) )
45	44	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) = ( 𝑥 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑥 ) )
46	37	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝑈 ∩ Ring ) ) )
47	46	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝑈 ∩ Ring ) )
48	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
49	47 48	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
50	31 32 15 33 49 49	ringchom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
51	30 45 50	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
52	12 29 51	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )