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 biimtrdi ⊢ ( 𝐵 = ( 𝑈 ∩ 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 ‘ 𝑥 ) ) ) ) )