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

Metamath Proof Explorer

Theorem rhmsubclem4

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

Ref Expression
Hypotheses rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubclem4 ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3 rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝜑 )
6 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝜑 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝑅 )
8 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
9 simpl ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑦 ∈ 𝑅 )
10 9 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
11 1 2 3 4 rhmsubclem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
12 6 8 10 11 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
13 12 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) )
14 simpr ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ 𝑅 )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑅 )
16 1 2 3 4 rhmsubclem2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
17 6 10 15 16 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
18 17 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) )
19 13 18 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ↔ ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) ) )
20 rhmco ⊢ ( ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ∧ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
21 20 ancoms ⊢ ( ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
22 19 21 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) ) )
23 22 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
24 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑈 ∈ 𝑉 )
25 2 eqcomi ⊢ ( RngCat ‘ 𝑈 ) = 𝐶
26 25 fveq2i ⊢ ( comp ‘ ( RngCat ‘ 𝑈 ) ) = ( comp ‘ 𝐶 )
27 inss2 ⊢ ( Ring ∩ 𝑈 ) ⊆ 𝑈
28 3 27 eqsstrdi ⊢ ( 𝜑 → 𝑅 ⊆ 𝑈 )
29 28 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝑈 )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑈 )
31 30 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ 𝑈 )
32 28 sseld ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑅 → 𝑦 ∈ 𝑈 ) )
33 32 adantrd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑦 ∈ 𝑈 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑦 ∈ 𝑈 ) )
35 34 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑈 )
36 35 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ 𝑈 )
37 28 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑅 → 𝑧 ∈ 𝑈 ) )
38 37 adantld ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ 𝑈 ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ 𝑈 ) )
40 39 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑧 ∈ 𝑈 )
41 40 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝑈 )
42 4 oveqi ⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 )
43 8 10 ovresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
44 42 43 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
45 44 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) )
46 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
47 eqid ⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
48 46 47 rhmf ⊢ ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
49 45 48 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
50 49 com12 ⊢ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
51 50 adantr ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
52 51 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
53 4 oveqi ⊢ ( 𝑦 𝐻 𝑧 ) = ( 𝑦 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑧 )
54 ovres ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑦 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
56 53 55 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
57 56 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ) )
58 eqid ⊢ ( Base ‘ 𝑧 ) = ( Base ‘ 𝑧 )
59 47 58 rhmf ⊢ ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
60 57 59 biimtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
61 60 com12 ⊢ ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
62 61 adantl ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
63 62 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
64 2 24 26 31 36 41 52 63 rngcco ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
65 1 2 3 4 rhmsubclem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
66 6 8 15 65 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
67 66 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
68 23 64 67 3eltr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑅 ) ∧ ( 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( RngCat ‘ 𝑈 ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )