Metamath Proof Explorer

Theorem rhmsubclem4

Description: Lemma 4 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u 
|- ( ph -> U e. V )
rngcrescrhm.c 
|- C = ( RngCat ` U )
rngcrescrhm.r 
|- ( ph -> R = ( Ring i^i U ) )
rngcrescrhm.h 
|- H = ( RingHom |` ( R X. R ) )
Assertion rhmsubclem4 
|- ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u 
 |-  ( ph -> U e. V )
2 rngcrescrhm.c 
 |-  C = ( RngCat ` U )
3 rngcrescrhm.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhm.h 
 |-  H = ( RingHom |` ( R X. R ) )
5 simpl 
 |-  ( ( ph /\ x e. R ) -> ph )
6 5 adantr 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ph )
7 simpr 
 |-  ( ( ph /\ x e. R ) -> x e. R )
8 7 adantr 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> x e. R )
9 simpl 
 |-  ( ( y e. R /\ z e. R ) -> y e. R )
10 9 adantl 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> y e. R )
11 1 2 3 4 rhmsubclem2 
 |-  ( ( ph /\ x e. R /\ y e. R ) -> ( x H y ) = ( x RingHom y ) )
12 6 8 10 11 syl3anc 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( x H y ) = ( x RingHom y ) )
13 12 eleq2d 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( f e. ( x H y ) <-> f e. ( x RingHom y ) ) )
14 simpr 
 |-  ( ( y e. R /\ z e. R ) -> z e. R )
15 14 adantl 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> z e. R )
16 1 2 3 4 rhmsubclem2 
 |-  ( ( ph /\ y e. R /\ z e. R ) -> ( y H z ) = ( y RingHom z ) )
17 6 10 15 16 syl3anc 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( y H z ) = ( y RingHom z ) )
18 17 eleq2d 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( g e. ( y H z ) <-> g e. ( y RingHom z ) ) )
19 13 18 anbi12d 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) <-> ( f e. ( x RingHom y ) /\ g e. ( y RingHom z ) ) ) )
20 rhmco 
 |-  ( ( g e. ( y RingHom z ) /\ f e. ( x RingHom y ) ) -> ( g o. f ) e. ( x RingHom z ) )
21 20 ancoms 
 |-  ( ( f e. ( x RingHom y ) /\ g e. ( y RingHom z ) ) -> ( g o. f ) e. ( x RingHom z ) )
22 19 21 biimtrdi 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( g o. f ) e. ( x RingHom z ) ) )
23 22 imp 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g o. f ) e. ( x RingHom z ) )
24 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> U e. V )
25 2 eqcomi 
 |-  ( RngCat ` U ) = C
26 25 fveq2i 
 |-  ( comp ` ( RngCat ` U ) ) = ( comp ` C )
27 inss2 
 |-  ( Ring i^i U ) C_ U
28 3 27 eqsstrdi 
 |-  ( ph -> R C_ U )
29 28 sselda 
 |-  ( ( ph /\ x e. R ) -> x e. U )
30 29 adantr 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> x e. U )
31 30 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x e. U )
32 28 sseld 
 |-  ( ph -> ( y e. R -> y e. U ) )
33 32 adantrd 
 |-  ( ph -> ( ( y e. R /\ z e. R ) -> y e. U ) )
34 33 adantr 
 |-  ( ( ph /\ x e. R ) -> ( ( y e. R /\ z e. R ) -> y e. U ) )
35 34 imp 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> y e. U )
36 35 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> y e. U )
37 28 sseld 
 |-  ( ph -> ( z e. R -> z e. U ) )
38 37 adantld 
 |-  ( ph -> ( ( y e. R /\ z e. R ) -> z e. U ) )
39 38 adantr 
 |-  ( ( ph /\ x e. R ) -> ( ( y e. R /\ z e. R ) -> z e. U ) )
40 39 imp 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> z e. U )
41 40 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> z e. U )
42 4 oveqi 
 |-  ( x H y ) = ( x ( RingHom |` ( R X. R ) ) y )
43 8 10 ovresd 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( x ( RingHom |` ( R X. R ) ) y ) = ( x RingHom y ) )
44 42 43 eqtrid 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( x H y ) = ( x RingHom y ) )
45 44 eleq2d 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( f e. ( x H y ) <-> f e. ( x RingHom y ) ) )
46 eqid 
 |-  ( Base ` x ) = ( Base ` x )
47 eqid 
 |-  ( Base ` y ) = ( Base ` y )
48 46 47 rhmf 
 |-  ( f e. ( x RingHom y ) -> f : ( Base ` x ) --> ( Base ` y ) )
49 45 48 biimtrdi 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( f e. ( x H y ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
50 49 com12 
 |-  ( f e. ( x H y ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
51 50 adantr 
 |-  ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
52 51 impcom 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f : ( Base ` x ) --> ( Base ` y ) )
53 4 oveqi 
 |-  ( y H z ) = ( y ( RingHom |` ( R X. R ) ) z )
54 ovres 
 |-  ( ( y e. R /\ z e. R ) -> ( y ( RingHom |` ( R X. R ) ) z ) = ( y RingHom z ) )
55 54 adantl 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( y ( RingHom |` ( R X. R ) ) z ) = ( y RingHom z ) )
56 53 55 eqtrid 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( y H z ) = ( y RingHom z ) )
57 56 eleq2d 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( g e. ( y H z ) <-> g e. ( y RingHom z ) ) )
58 eqid 
 |-  ( Base ` z ) = ( Base ` z )
59 47 58 rhmf 
 |-  ( g e. ( y RingHom z ) -> g : ( Base ` y ) --> ( Base ` z ) )
60 57 59 biimtrdi 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( g e. ( y H z ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
61 60 com12 
 |-  ( g e. ( y H z ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
62 61 adantl 
 |-  ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
63 62 impcom 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g : ( Base ` y ) --> ( Base ` z ) )
64 2 24 26 31 36 41 52 63 rngcco 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) = ( g o. f ) )
65 1 2 3 4 rhmsubclem2 
 |-  ( ( ph /\ x e. R /\ z e. R ) -> ( x H z ) = ( x RingHom z ) )
66 6 8 15 65 syl3anc 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( x H z ) = ( x RingHom z ) )
67 66 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x H z ) = ( x RingHom z ) )
68 23 64 67 3eltr4d 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCat ` U ) ) z ) f ) e. ( x H z ) )