Metamath Proof Explorer

Theorem rngccoALTV

Description: Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbasALTV.c 
|- C = ( RngCatALTV ` U )
rngcbasALTV.b 
|- B = ( Base ` C )
rngcbasALTV.u 
|- ( ph -> U e. V )
rngccofvalALTV.o 
|- .x. = ( comp ` C )
rngccoALTV.x 
|- ( ph -> X e. B )
rngccoALTV.y 
|- ( ph -> Y e. B )
rngccoALTV.z 
|- ( ph -> Z e. B )
rngccoALTV.f 
|- ( ph -> F e. ( X RngHomo Y ) )
rngccoALTV.g 
|- ( ph -> G e. ( Y RngHomo Z ) )
Assertion rngccoALTV 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )

Proof

Step Hyp Ref Expression
1 rngcbasALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngcbasALTV.b 
 |-  B = ( Base ` C )
3 rngcbasALTV.u 
 |-  ( ph -> U e. V )
4 rngccofvalALTV.o 
 |-  .x. = ( comp ` C )
5 rngccoALTV.x 
 |-  ( ph -> X e. B )
6 rngccoALTV.y 
 |-  ( ph -> Y e. B )
7 rngccoALTV.z 
 |-  ( ph -> Z e. B )
8 rngccoALTV.f 
 |-  ( ph -> F e. ( X RngHomo Y ) )
9 rngccoALTV.g 
 |-  ( ph -> G e. ( Y RngHomo Z ) )
10 1 2 3 4 rngccofvalALTV 
 |-  ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
11 simprl 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> v = <. X , Y >. )
12 11 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = ( 2nd ` <. X , Y >. ) )
13 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
14 5 6 13 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
15 14 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
16 12 15 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` v ) = Y )
17 simprr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> z = Z )
18 16 17 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( 2nd ` v ) RngHomo z ) = ( Y RngHomo Z ) )
19 11 fveq2d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` v ) = ( 1st ` <. X , Y >. ) )
20 op1stg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
21 5 6 20 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
22 21 adantr 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` <. X , Y >. ) = X )
23 19 22 eqtrd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( 1st ` v ) = X )
24 23 16 oveq12d 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) = ( X RngHomo Y ) )
25 eqidd 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g o. f ) = ( g o. f ) )
26 18 24 25 mpoeq123dv 
 |-  ( ( ph /\ ( v = <. X , Y >. /\ z = Z ) ) -> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) = ( g e. ( Y RngHomo Z ) , f e. ( X RngHomo Y ) |-> ( g o. f ) ) )
27 opelxpi 
 |-  ( ( X e. B /\ Y e. B ) -> <. X , Y >. e. ( B X. B ) )
28 5 6 27 syl2anc 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
29 ovex 
 |-  ( Y RngHomo Z ) e. _V
30 ovex 
 |-  ( X RngHomo Y ) e. _V
31 29 30 mpoex 
 |-  ( g e. ( Y RngHomo Z ) , f e. ( X RngHomo Y ) |-> ( g o. f ) ) e. _V
32 31 a1i 
 |-  ( ph -> ( g e. ( Y RngHomo Z ) , f e. ( X RngHomo Y ) |-> ( g o. f ) ) e. _V )
33 10 26 28 7 32 ovmpod 
 |-  ( ph -> ( <. X , Y >. .x. Z ) = ( g e. ( Y RngHomo Z ) , f e. ( X RngHomo Y ) |-> ( g o. f ) ) )
34 simprl 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> g = G )
35 simprr 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> f = F )
36 34 35 coeq12d 
 |-  ( ( ph /\ ( g = G /\ f = F ) ) -> ( g o. f ) = ( G o. F ) )
37 coexg 
 |-  ( ( G e. ( Y RngHomo Z ) /\ F e. ( X RngHomo Y ) ) -> ( G o. F ) e. _V )
38 9 8 37 syl2anc 
 |-  ( ph -> ( G o. F ) e. _V )
39 33 36 9 8 38 ovmpod 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) = ( G o. F ) )