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

Metamath Proof Explorer

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 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 ⊢ ( 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 ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )