Theorem rhmsubcsetclem1

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

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

Proof

Step	Hyp	Ref	Expression
1		rhmsubcsetc.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2		rhmsubcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		rhmsubcsetc.b	⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
4		rhmsubcsetc.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	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
14	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ 𝑉 )
15	6	simprbi	⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ 𝑈 )
16	5 15	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
17	16	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
18	1 13 14 17	estrcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
19	4	oveqdr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
20		eqid	⊢ ( RingCat ‘ 𝑈 ) = ( RingCat ‘ 𝑈 )
21		eqid	⊢ ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( Base ‘ ( RingCat ‘ 𝑈 ) )
22		eqid	⊢ ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( Hom ‘ ( RingCat ‘ 𝑈 ) )
23	20 21 2 22	ringchomfval	⊢ ( 𝜑 → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) ) )
24	20 21 2	ringcbas	⊢ ( 𝜑 → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
25		incom	⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
26	3 25	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
27	26	eqcomd	⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) = 𝐵 )
28	24 27	eqtrd	⊢ ( 𝜑 → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = 𝐵 )
29	28	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) = ( 𝐵 × 𝐵 ) )
30	29	reseq2d	⊢ ( 𝜑 → ( RingHom ↾ ( ( Base ‘ ( RingCat ‘ 𝑈 ) ) × ( Base ‘ ( RingCat ‘ 𝑈 ) ) ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
31	23 30	eqtrd	⊢ ( 𝜑 → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Hom ‘ ( RingCat ‘ 𝑈 ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
33	32	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) = ( Hom ‘ ( RingCat ‘ 𝑈 ) ) )
34	33	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) = ( 𝑥 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑥 ) )
35	26	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝑈 ∩ Ring ) ) )
36	35	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝑈 ∩ Ring ) )
37	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Base ‘ ( RingCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Ring ) )
38	36 37	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ ( RingCat ‘ 𝑈 ) ) )
39	20 21 14 22 38 38	ringchom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( Hom ‘ ( RingCat ‘ 𝑈 ) ) 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
40	19 34 39	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
41	12 18 40	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )