This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rnghmsubcsetclem1 ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Proof

Step Hyp Ref Expression
1 rnghmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 rnghmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rnghmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
4 rnghmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
5 3 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Rng ∩ 𝑈 ) ) )
6 elin ⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) ↔ ( 𝑥 ∈ Rng ∧ 𝑥 ∈ 𝑈 ) )
7 6 simplbi ⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) → 𝑥 ∈ Rng )
8 5 7 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ Rng ) )
9 8 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ Rng )
10 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
11 10 idrnghm ⊢ ( 𝑥 ∈ Rng → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RngHom 𝑥 ) )
12 9 11 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RngHom 𝑥 ) )
13 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑈 ∈ 𝑉 )
15 6 simprbi ⊢ ( 𝑥 ∈ ( Rng ∩ 𝑈 ) → 𝑥 ∈ 𝑈 )
16 5 15 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
17 16 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
18 1 13 14 17 estrcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
19 4 oveqdr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 ( RngHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
20 eqid ⊢ ( RngCat ‘ 𝑈 ) = ( RngCat ‘ 𝑈 )
21 eqid ⊢ ( Base ‘ ( RngCat ‘ 𝑈 ) ) = ( Base ‘ ( RngCat ‘ 𝑈 ) )
22 eqid ⊢ ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( Hom ‘ ( RngCat ‘ 𝑈 ) )
23 20 21 2 22 rngchomfval ⊢ ( 𝜑 → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHom ↾ ( ( 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 ⊢ ( 𝜑 → ( RngHom ↾ ( ( Base ‘ ( RngCat ‘ 𝑈 ) ) × ( Base ‘ ( RngCat ‘ 𝑈 ) ) ) ) = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
31 23 30 eqtrd ⊢ ( 𝜑 → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( Hom ‘ ( RngCat ‘ 𝑈 ) ) = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
33 32 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( RngHom ↾ ( 𝐵 × 𝐵 ) ) = ( Hom ‘ ( RngCat ‘ 𝑈 ) ) )
34 33 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( RngHom ↾ ( 𝐵 × 𝐵 ) ) 𝑥 ) = ( 𝑥 ( 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 ‘ 𝑈 ) ) 𝑥 ) = ( 𝑥 RngHom 𝑥 ) )
40 19 34 39 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RngHom 𝑥 ) )
41 12 18 40 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )