Metamath Proof Explorer


Theorem ringccatidALTV

Description: Lemma for ringccatALTV . (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringccatALTV.c 𝐶 = ( RingCatALTV ‘ 𝑈 )
ringccatidALTV.b 𝐵 = ( Base ‘ 𝐶 )
Assertion ringccatidALTV ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ringccatALTV.c 𝐶 = ( RingCatALTV ‘ 𝑈 )
2 ringccatidALTV.b 𝐵 = ( Base ‘ 𝐶 )
3 2 a1i ( 𝑈𝑉𝐵 = ( Base ‘ 𝐶 ) )
4 eqidd ( 𝑈𝑉 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
5 eqidd ( 𝑈𝑉 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
6 1 fvexi 𝐶 ∈ V
7 6 a1i ( 𝑈𝑉𝐶 ∈ V )
8 biid ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ↔ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) )
9 simpl ( ( 𝑈𝑉𝑥𝐵 ) → 𝑈𝑉 )
10 1 2 9 ringcbasALTV ( ( 𝑈𝑉𝑥𝐵 ) → 𝐵 = ( 𝑈 ∩ Ring ) )
11 eleq2 ( 𝐵 = ( 𝑈 ∩ Ring ) → ( 𝑥𝐵𝑥 ∈ ( 𝑈 ∩ Ring ) ) )
12 elin ( 𝑥 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑥𝑈𝑥 ∈ Ring ) )
13 12 simprbi ( 𝑥 ∈ ( 𝑈 ∩ Ring ) → 𝑥 ∈ Ring )
14 11 13 syl6bi ( 𝐵 = ( 𝑈 ∩ Ring ) → ( 𝑥𝐵𝑥 ∈ Ring ) )
15 14 com12 ( 𝑥𝐵 → ( 𝐵 = ( 𝑈 ∩ Ring ) → 𝑥 ∈ Ring ) )
16 15 adantl ( ( 𝑈𝑉𝑥𝐵 ) → ( 𝐵 = ( 𝑈 ∩ Ring ) → 𝑥 ∈ Ring ) )
17 10 16 mpd ( ( 𝑈𝑉𝑥𝐵 ) → 𝑥 ∈ Ring )
18 eqid ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
19 18 idrhm ( 𝑥 ∈ Ring → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
20 17 19 syl ( ( 𝑈𝑉𝑥𝐵 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
21 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
22 simpr ( ( 𝑈𝑉𝑥𝐵 ) → 𝑥𝐵 )
23 1 2 9 21 22 22 ringchomALTV ( ( 𝑈𝑉𝑥𝐵 ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑥 RingHom 𝑥 ) )
24 20 23 eleqtrrd ( ( 𝑈𝑉𝑥𝐵 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
25 simpl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑈𝑉 )
26 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
27 simpl ( ( 𝑤𝐵𝑥𝐵 ) → 𝑤𝐵 )
28 27 3ad2ant1 ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑤𝐵 )
29 28 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑤𝐵 )
30 simpr ( ( 𝑤𝐵𝑥𝐵 ) → 𝑥𝐵 )
31 30 3ad2ant1 ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥𝐵 )
32 31 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑥𝐵 )
33 simp1 ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑈𝑉 )
34 27 3ad2ant3 ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑤𝐵 )
35 30 3ad2ant3 ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑥𝐵 )
36 1 2 33 21 34 35 ringchomALTV ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑤 RingHom 𝑥 ) )
37 36 eleq2d ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ 𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) )
38 37 biimpd ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → 𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) )
39 38 3exp ( 𝑈𝑉 → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → 𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) ) ) )
40 39 com14 ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) ) ) )
41 40 3ad2ant1 ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) ) ) )
42 41 com13 ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) ) ) )
43 42 3imp ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) )
44 43 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 RingHom 𝑥 ) )
45 20 expcom ( 𝑥𝐵 → ( 𝑈𝑉 → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) ) )
46 45 adantl ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉 → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) ) )
47 46 3ad2ant1 ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉 → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) ) )
48 47 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
49 1 2 25 26 29 32 32 44 48 ringccoALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) )
50 simpl ( ( 𝑈𝑉 ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑈𝑉 )
51 simprl ( ( 𝑈𝑉 ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑤𝐵 )
52 simprr ( ( 𝑈𝑉 ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑥𝐵 )
53 1 2 50 21 51 52 elringchomALTV ( ( 𝑈𝑉 ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) )
54 53 ex ( 𝑈𝑉 → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) ) )
55 54 com13 ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) ) )
56 fcoi2 ( 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 )
57 55 56 syl8 ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉 → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) ) )
58 57 3ad2ant1 ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉 → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) ) )
59 58 com12 ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉 → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) ) )
60 59 a1d ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉 → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) ) ) )
61 60 3imp ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉 → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 ) )
62 61 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 )
63 49 62 eqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
64 simp3 ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → 𝑈𝑉 )
65 30 adantr ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑥𝐵 )
66 65 3ad2ant2 ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → 𝑥𝐵 )
67 simprl ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → 𝑦𝐵 )
68 67 3ad2ant2 ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → 𝑦𝐵 )
69 46 adantr ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉 → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) ) )
70 69 a1i ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉 → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) ) ) )
71 70 3imp ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 RingHom 𝑥 ) )
72 simpl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → 𝑈𝑉 )
73 65 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → 𝑥𝐵 )
74 67 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → 𝑦𝐵 )
75 1 2 72 21 73 74 ringchomALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
76 75 eleq2d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) )
77 76 biimpd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) )
78 77 ex ( 𝑈𝑉 → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) )
79 78 com13 ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) )
80 79 3imp ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) )
81 1 2 64 26 66 66 68 71 80 ringccoALTV ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
82 1 2 72 21 73 74 elringchomALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
83 82 ex ( 𝑈𝑉 → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) ) )
84 83 com13 ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) ) )
85 84 3imp ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
86 fcoi1 ( 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
87 85 86 syl ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
88 81 87 eqtrd ( ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) ∧ 𝑈𝑉 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
89 88 3exp ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉 → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) ) )
90 89 3ad2ant2 ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ) → ( 𝑈𝑉 → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) ) )
91 90 expdcom ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉 → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) ) ) )
92 91 3imp ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉 → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 ) )
93 92 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
94 simpl ( ( 𝑦𝐵𝑧𝐵 ) → 𝑦𝐵 )
95 94 3ad2ant2 ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑦𝐵 )
96 1 2 33 21 35 95 ringchomALTV ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 RingHom 𝑦 ) )
97 96 eleq2d ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) )
98 97 biimpd ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) )
99 98 3exp ( 𝑈𝑉 → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) ) )
100 99 com14 ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) ) )
101 100 3ad2ant2 ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) ) )
102 101 com13 ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) ) ) )
103 102 3imp ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) )
104 103 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) )
105 rhmco ( ( 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ∧ 𝑓 ∈ ( 𝑤 RingHom 𝑥 ) ) → ( 𝑔𝑓 ) ∈ ( 𝑤 RingHom 𝑦 ) )
106 104 44 105 syl2anc ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔𝑓 ) ∈ ( 𝑤 RingHom 𝑦 ) )
107 94 3ad2ant2 ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦𝐵 )
108 107 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑦𝐵 )
109 1 2 25 26 29 32 108 44 104 ringccoALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = ( 𝑔𝑓 ) )
110 1 2 25 21 29 108 ringchomALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑤 RingHom 𝑦 ) )
111 106 109 110 3eltr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) )
112 coass ( ( 𝑔 ) ∘ 𝑓 ) = ( ∘ ( 𝑔𝑓 ) )
113 simp2r ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧𝐵 )
114 113 adantl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧𝐵 )
115 simp2r ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → 𝑧𝐵 )
116 1 2 33 21 95 115 ringchomALTV ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( 𝑦 RingHom 𝑧 ) )
117 116 eleq2d ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↔ ∈ ( 𝑦 RingHom 𝑧 ) ) )
118 117 biimpd ( ( 𝑈𝑉 ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑤𝐵𝑥𝐵 ) ) → ( ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) → ∈ ( 𝑦 RingHom 𝑧 ) ) )
119 118 3exp ( 𝑈𝑉 → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) → ∈ ( 𝑦 RingHom 𝑧 ) ) ) ) )
120 119 com14 ( ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉 ∈ ( 𝑦 RingHom 𝑧 ) ) ) ) )
121 120 3ad2ant3 ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑤𝐵𝑥𝐵 ) → ( 𝑈𝑉 ∈ ( 𝑦 RingHom 𝑧 ) ) ) ) )
122 121 com13 ( ( 𝑤𝐵𝑥𝐵 ) → ( ( 𝑦𝐵𝑧𝐵 ) → ( ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( 𝑈𝑉 ∈ ( 𝑦 RingHom 𝑧 ) ) ) ) )
123 122 3imp ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈𝑉 ∈ ( 𝑦 RingHom 𝑧 ) ) )
124 123 impcom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ∈ ( 𝑦 RingHom 𝑧 ) )
125 rhmco ( ( ∈ ( 𝑦 RingHom 𝑧 ) ∧ 𝑔 ∈ ( 𝑥 RingHom 𝑦 ) ) → ( 𝑔 ) ∈ ( 𝑥 RingHom 𝑧 ) )
126 124 104 125 syl2anc ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ) ∈ ( 𝑥 RingHom 𝑧 ) )
127 1 2 25 26 29 32 114 44 126 ringccoALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( 𝑔 ) ∘ 𝑓 ) )
128 1 2 25 26 29 108 114 106 124 ringccoALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) = ( ∘ ( 𝑔𝑓 ) ) )
129 112 127 128 3eqtr4a ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) )
130 1 2 25 26 32 108 114 104 124 ringccoALTV ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) = ( 𝑔 ) )
131 130 oveq1d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
132 109 oveq2d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) )
133 129 131 132 3eqtr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
134 3 4 5 7 8 24 63 93 111 133 iscatd2 ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )