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	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑅 → 𝑥 ∈ 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 ‘ 𝑈 ) ) ‘ 𝑥 ) ∈ ( 𝑥 𝐻 𝑥 ) )