Theorem rnghmsubcsetclem1

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

	Ref	Expression
Hypotheses	rnghmsubcsetc.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
	rnghmsubcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rnghmsubcsetc.b	⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
	rnghmsubcsetc.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
Assertion	rnghmsubcsetclem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		rnghmsubcsetc.c	⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2		rnghmsubcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		rnghmsubcsetc.b	⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
4		rnghmsubcsetc.h	⊢ ( 𝜑 → 𝐻 = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
5	3	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Rng ∩ 𝑈 ) ) )
6		elin	⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) ↔ ( 𝑥 ∈ Rng ∧ 𝑥 ∈ 𝑈 ) )
7	6	simplbi	⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) → 𝑥 ∈ Rng )
8	5 7	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ Rng ) )
9	8	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ Rng )
10		eqid	⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
11	10	idrnghm	⊢ ( 𝑥 ∈ Rng → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RngHomo 𝑥 ) )
12	9 11	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RngHomo 𝑥 ) )
13		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
14	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ 𝑉 )
15	6	simprbi	⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) → 𝑥 ∈ 𝑈 )
16	5 15	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
17	16	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
18	1 13 14 17	estrcid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
19	4	oveqdr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
20		eqid	⊢ ( RngCat ‘ 𝑈 ) = ( RngCat ‘ 𝑈 )
21		eqid	⊢ ( Base ‘ ( RngCat ‘ 𝑈 ) ) = ( Base ‘ ( RngCat ‘ 𝑈 ) )
22		eqid	⊢ ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( Hom ‘ ( RngCat ‘ 𝑈 ) )
23	20 21 2 22	rngchomfval	⊢ ( 𝜑 → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHomo ↾ ( ( Base ‘ ( RngCat ‘ 𝑈 ) ) × ( Base ‘ ( RngCat ‘ 𝑈 ) ) ) ) )
24	20 21 2	rngcbas	⊢ ( 𝜑 → ( Base ‘ ( RngCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Rng ) )
25		incom	⊢ ( Rng ∩ 𝑈 ) = ( 𝑈 ∩ Rng )
26	3 25	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
27	26	eqcomd	⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = 𝐵 )
28	24 27	eqtrd	⊢ ( 𝜑 → ( Base ‘ ( RngCat ‘ 𝑈 ) ) = 𝐵 )
29	28	sqxpeqd	⊢ ( 𝜑 → ( ( Base ‘ ( RngCat ‘ 𝑈 ) ) × ( Base ‘ ( RngCat ‘ 𝑈 ) ) ) = ( 𝐵 × 𝐵 ) )
30	29	reseq2d	⊢ ( 𝜑 → ( RngHomo ↾ ( ( Base ‘ ( RngCat ‘ 𝑈 ) ) × ( Base ‘ ( RngCat ‘ 𝑈 ) ) ) ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
31	23 30	eqtrd	⊢ ( 𝜑 → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
33	32	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) = ( Hom ‘ ( RngCat ‘ 𝑈 ) ) )
34	33	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) = ( 𝑥 ( Hom ‘ ( RngCat ‘ 𝑈 ) ) 𝑥 ) )
35	26	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝑈 ∩ Rng ) ) )
36	35	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝑈 ∩ Rng ) )
37	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Base ‘ ( RngCat ‘ 𝑈 ) ) = ( 𝑈 ∩ Rng ) )
38	36 37	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ ( RngCat ‘ 𝑈 ) ) )
39	20 21 14 22 38 38	rngchom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( Hom ‘ ( RngCat ‘ 𝑈 ) ) 𝑥 ) = ( 𝑥 RngHomo 𝑥 ) )
40	19 34 39	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RngHomo 𝑥 ) )
41	12 18 40	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )