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

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 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 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
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 ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )