Metamath Proof Explorer

Theorem rhmsubcsetclem2

Description: Lemma 2 for rhmsubcsetc . (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rhmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
rhmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rhmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
rhmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rhmsubcsetclem2 ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c ⊢ 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 rhmsubcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 rhmsubcsetc.b ⊢ ( 𝜑 → 𝐵 = ( Ring ∩ 𝑈 ) )
4 rhmsubcsetc.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
6 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 )
7 6 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝜑 )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) )
9 8 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) )
10 simpr ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
11 10 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
12 4 rhmresel ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) )
13 7 9 11 12 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
15 simpl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
16 14 15 anim12i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
17 16 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
18 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
19 4 rhmresel ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) )
20 7 17 18 19 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) )
21 rhmco ⊢ ( ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) ∧ 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
22 13 20 21 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( 𝑥 RingHom 𝑧 ) )
23 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑈 ∈ 𝑉 )
24 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
25 3 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Ring ∩ 𝑈 ) ) )
26 elinel2 ⊢ ( 𝑥 ∈ ( Ring ∩ 𝑈 ) → 𝑥 ∈ 𝑈 )
27 25 26 syl6bi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
28 27 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑈 )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑥 ∈ 𝑈 )
31 3 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Ring ∩ 𝑈 ) ) )
32 elinel2 ⊢ ( 𝑦 ∈ ( Ring ∩ 𝑈 ) → 𝑦 ∈ 𝑈 )
33 31 32 syl6bi ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈 ) )
35 34 com12 ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑦 ∈ 𝑈 ) )
36 35 adantr ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑦 ∈ 𝑈 ) )
37 36 impcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝑈 )
38 37 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑦 ∈ 𝑈 )
39 3 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( Ring ∩ 𝑈 ) ) )
40 elinel2 ⊢ ( 𝑧 ∈ ( Ring ∩ 𝑈 ) → 𝑧 ∈ 𝑈 )
41 39 40 syl6bi ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝑈 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝑈 ) )
43 42 adantld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝑈 ) )
44 43 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝑈 )
45 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝑈 )
46 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
47 eqid ⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
48 eqid ⊢ ( Base ‘ 𝑧 ) = ( Base ‘ 𝑧 )
49 simprl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) → 𝜑 )
50 49 adantr ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝜑 )
51 14 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
52 51 ancoms ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
53 52 adantr ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
54 simpr ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
55 50 53 54 19 syl3anc ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) )
56 46 47 rhmf ⊢ ( 𝑓 ∈ ( 𝑥 RingHom 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
57 55 56 syl ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) ∧ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
58 57 ex ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
59 58 ex ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) ) )
60 59 adantr ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) ) )
61 60 impcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
62 61 com12 ⊢ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
63 62 adantr ⊢ ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
64 63 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑓 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
65 12 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) )
66 47 48 rhmf ⊢ ( 𝑔 ∈ ( 𝑦 RingHom 𝑧 ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
67 65 66 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
68 67 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
69 68 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
70 69 adantld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
71 70 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → 𝑔 : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
72 1 23 24 30 38 45 46 47 48 64 71 estrcco ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
73 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
74 73 oveqdr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑧 ) )
75 ovres ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
76 75 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 ( RingHom ↾ ( 𝐵 × 𝐵 ) ) 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
77 74 76 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
78 77 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑥 𝐻 𝑧 ) = ( 𝑥 RingHom 𝑧 ) )
79 22 72 78 3eltr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
80 79 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
81 80 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )