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

Metamath Proof Explorer

Theorem rhmsubcrngclem2

Description: Lemma 2 for rhmsubcrngc . (Contributed by AV, 12-Mar-2020)

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

Proof

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