Metamath Proof Explorer

Theorem rhmsubcrngclem2

Description: Lemma 2 for rhmsubcrngc . (Contributed by AV, 12-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c 
 |-  C = ( RngCat ` U )
2 rhmsubcrngc.u 
 |-  ( ph -> U e. V )
3 rhmsubcrngc.b 
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcrngc.h 
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 simpl 
 |-  ( ( ph /\ x e. B ) -> ph )
6 5 ad2antrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ph )
7 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( y e. B /\ z e. B ) )
8 7 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( y e. B /\ z e. B ) )
9 simprr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g e. ( y H z ) )
10 4 rhmresel 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) /\ g e. ( y H z ) ) -> g e. ( y RingHom z ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g e. ( y RingHom z ) )
12 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
13 simpl 
 |-  ( ( y e. B /\ z e. B ) -> y e. B )
14 12 13 anim12i 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( x e. B /\ y e. B ) )
15 14 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x e. B /\ y e. B ) )
16 simprl 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f e. ( x H y ) )
17 4 rhmresel 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ f e. ( x H y ) ) -> f e. ( x RingHom y ) )
18 6 15 16 17 syl3anc 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f e. ( x RingHom y ) )
19 rhmco 
 |-  ( ( g e. ( y RingHom z ) /\ f e. ( x RingHom y ) ) -> ( g o. f ) e. ( x RingHom z ) )
20 11 18 19 syl2anc 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g o. f ) e. ( x RingHom z ) )
21 2 adantr 
 |-  ( ( ph /\ x e. B ) -> U e. V )
22 21 ad2antrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> U e. V )
23 eqid 
 |-  ( comp ` C ) = ( comp ` C )
24 3 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Ring i^i U ) ) )
25 elinel2 
 |-  ( x e. ( Ring i^i U ) -> x e. U )
26 24 25 syl6bi 
 |-  ( ph -> ( x e. B -> x e. U ) )
27 26 imp 
 |-  ( ( ph /\ x e. B ) -> x e. U )
28 27 ad2antrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x e. U )
29 3 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Ring i^i U ) ) )
30 elinel2 
 |-  ( y e. ( Ring i^i U ) -> y e. U )
31 29 30 syl6bi 
 |-  ( ph -> ( y e. B -> y e. U ) )
32 31 adantr 
 |-  ( ( ph /\ x e. B ) -> ( y e. B -> y e. U ) )
33 32 com12 
 |-  ( y e. B -> ( ( ph /\ x e. B ) -> y e. U ) )
34 33 adantr 
 |-  ( ( y e. B /\ z e. B ) -> ( ( ph /\ x e. B ) -> y e. U ) )
35 34 impcom 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> y e. U )
36 35 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> y e. U )
37 3 eleq2d 
 |-  ( ph -> ( z e. B <-> z e. ( Ring i^i U ) ) )
38 elinel2 
 |-  ( z e. ( Ring i^i U ) -> z e. U )
39 37 38 syl6bi 
 |-  ( ph -> ( z e. B -> z e. U ) )
40 39 adantr 
 |-  ( ( ph /\ x e. B ) -> ( z e. B -> z e. U ) )
41 40 adantld 
 |-  ( ( ph /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> z e. U ) )
42 41 imp 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> z e. U )
43 42 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> z e. U )
44 simprl 
 |-  ( ( y e. B /\ ( ph /\ x e. B ) ) -> ph )
45 44 adantr 
 |-  ( ( ( y e. B /\ ( ph /\ x e. B ) ) /\ f e. ( x H y ) ) -> ph )
46 12 anim1i 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x e. B /\ y e. B ) )
47 46 ancoms 
 |-  ( ( y e. B /\ ( ph /\ x e. B ) ) -> ( x e. B /\ y e. B ) )
48 47 adantr 
 |-  ( ( ( y e. B /\ ( ph /\ x e. B ) ) /\ f e. ( x H y ) ) -> ( x e. B /\ y e. B ) )
49 simpr 
 |-  ( ( ( y e. B /\ ( ph /\ x e. B ) ) /\ f e. ( x H y ) ) -> f e. ( x H y ) )
50 45 48 49 17 syl3anc 
 |-  ( ( ( y e. B /\ ( ph /\ x e. B ) ) /\ f e. ( x H y ) ) -> f e. ( x RingHom y ) )
51 eqid 
 |-  ( Base ` x ) = ( Base ` x )
52 eqid 
 |-  ( Base ` y ) = ( Base ` y )
53 51 52 rhmf 
 |-  ( f e. ( x RingHom y ) -> f : ( Base ` x ) --> ( Base ` y ) )
54 50 53 syl 
 |-  ( ( ( y e. B /\ ( ph /\ x e. B ) ) /\ f e. ( x H y ) ) -> f : ( Base ` x ) --> ( Base ` y ) )
55 54 exp31 
 |-  ( y e. B -> ( ( ph /\ x e. B ) -> ( f e. ( x H y ) -> f : ( Base ` x ) --> ( Base ` y ) ) ) )
56 55 adantr 
 |-  ( ( y e. B /\ z e. B ) -> ( ( ph /\ x e. B ) -> ( f e. ( x H y ) -> f : ( Base ` x ) --> ( Base ` y ) ) ) )
57 56 impcom 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( f e. ( x H y ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
58 57 com12 
 |-  ( f e. ( x H y ) -> ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
59 58 adantr 
 |-  ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> f : ( Base ` x ) --> ( Base ` y ) ) )
60 59 impcom 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f : ( Base ` x ) --> ( Base ` y ) )
61 10 3expa 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y H z ) ) -> g e. ( y RingHom z ) )
62 eqid 
 |-  ( Base ` z ) = ( Base ` z )
63 52 62 rhmf 
 |-  ( g e. ( y RingHom z ) -> g : ( Base ` y ) --> ( Base ` z ) )
64 61 63 syl 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y H z ) ) -> g : ( Base ` y ) --> ( Base ` z ) )
65 64 ex 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y H z ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
66 65 adantlr 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( g e. ( y H z ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
67 66 adantld 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> g : ( Base ` y ) --> ( Base ` z ) ) )
68 67 imp 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g : ( Base ` y ) --> ( Base ` z ) )
69 1 22 23 28 36 43 60 68 rngcco 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g o. f ) )
70 4 adantr 
 |-  ( ( ph /\ x e. B ) -> H = ( RingHom |` ( B X. B ) ) )
71 70 oveqdr 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( x H z ) = ( x ( RingHom |` ( B X. B ) ) z ) )
72 ovres 
 |-  ( ( x e. B /\ z e. B ) -> ( x ( RingHom |` ( B X. B ) ) z ) = ( x RingHom z ) )
73 72 ad2ant2l 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( x ( RingHom |` ( B X. B ) ) z ) = ( x RingHom z ) )
74 71 73 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( x H z ) = ( x RingHom z ) )
75 74 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( x H z ) = ( x RingHom z ) )
76 20 69 75 3eltr4d 
 |-  ( ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) )
77 76 ralrimivva 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) )
78 77 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x H z ) )