Metamath Proof Explorer

Theorem ringccatidALTV

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

Ref Expression
Hypotheses ringccatALTV.c 
|- C = ( RingCatALTV ` U )
ringccatidALTV.b 
|- B = ( Base ` C )
Assertion ringccatidALTV 
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )

Proof

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