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

Metamath Proof Explorer

Theorem rhmsubclem3

Description: Lemma 3 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubclem3 ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3 rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 3 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 ↔ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) )
6 elinel1 ⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ Ring )
7 5 6 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 → 𝑥 ∈ Ring ) )
8 7 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ Ring )
9 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
10 9 idrhm ⊢ ( 𝑥 ∈ Ring → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
11 8 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
12 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13 2 eqcomi ⊢ ( RngCat ‘ 𝑈 ) = 𝐶
14 13 fveq2i ⊢ ( Id ‘ ( RngCat ‘ 𝑈 ) ) = ( Id ‘ 𝐶 )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑈 ∈ 𝑉 )
16 incom ⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
17 ringssrng ⊢ Ring ⊆ Rng
18 sslin ⊢ ( Ring ⊆ Rng → ( 𝑈 ∩ Ring ) ⊆ ( 𝑈 ∩ Rng ) )
19 17 18 mp1i ⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ⊆ ( 𝑈 ∩ Rng ) )
20 16 19 eqsstrid ⊢ ( 𝜑 → ( Ring ∩ 𝑈 ) ⊆ ( 𝑈 ∩ Rng ) )
21 2 12 1 rngcbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
22 20 3 21 3sstr4d ⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝐶 ) )
23 22 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
24 2 12 14 15 23 9 rngcid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) = ( I ↾ ( Base ‘ 𝑥 ) ) )
25 1 2 3 4 rhmsubclem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
26 25 3anidm23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
27 11 24 26 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( Id ‘ ( RngCat ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )