Metamath Proof Explorer

Theorem rhmsubcsetclem2

Description: Lemma 2 for rhmsubcsetc . (Contributed by AV, 9-Mar-2020)

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