Metamath Proof Explorer

Theorem rhmsubcALTVlem4

Description: Lemma 4 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u 
 |-  ( ph -> U e. V )
2 rngcrescrhmALTV.c 
 |-  C = ( RngCatALTV ` U )
3 rngcrescrhmALTV.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhmALTV.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 rhmsubcALTVlem2 
 |-  ( ( 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 rhmsubcALTVlem2 
 |-  ( ( 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 syl6bi 
 |-  ( ( ( 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 eqid 
 |-  ( RngCatALTV ` U ) = ( RngCatALTV ` U )
25 eqid 
 |-  ( Base ` ( RngCatALTV ` U ) ) = ( Base ` ( RngCatALTV ` U ) )
26 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 )
27 eqid 
 |-  ( comp ` ( RngCatALTV ` U ) ) = ( comp ` ( RngCatALTV ` U ) )
28 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
29 ringrng 
 |-  ( x e. Ring -> x e. Rng )
30 29 a1i 
 |-  ( ph -> ( x e. Ring -> x e. Rng ) )
31 30 ssrdv 
 |-  ( ph -> Ring C_ Rng )
32 sslin 
 |-  ( Ring C_ Rng -> ( U i^i Ring ) C_ ( U i^i Rng ) )
33 31 32 syl 
 |-  ( ph -> ( U i^i Ring ) C_ ( U i^i Rng ) )
34 28 33 eqsstrid 
 |-  ( ph -> ( Ring i^i U ) C_ ( U i^i Rng ) )
35 24 25 1 rngcbasALTV 
 |-  ( ph -> ( Base ` ( RngCatALTV ` U ) ) = ( U i^i Rng ) )
36 34 3 35 3sstr4d 
 |-  ( ph -> R C_ ( Base ` ( RngCatALTV ` U ) ) )
37 36 sselda 
 |-  ( ( ph /\ x e. R ) -> x e. ( Base ` ( RngCatALTV ` U ) ) )
38 37 adantr 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> x e. ( Base ` ( RngCatALTV ` U ) ) )
39 38 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> x e. ( Base ` ( RngCatALTV ` U ) ) )
40 36 sseld 
 |-  ( ph -> ( y e. R -> y e. ( Base ` ( RngCatALTV ` U ) ) ) )
41 40 adantr 
 |-  ( ( ph /\ x e. R ) -> ( y e. R -> y e. ( Base ` ( RngCatALTV ` U ) ) ) )
42 41 com12 
 |-  ( y e. R -> ( ( ph /\ x e. R ) -> y e. ( Base ` ( RngCatALTV ` U ) ) ) )
43 42 adantr 
 |-  ( ( y e. R /\ z e. R ) -> ( ( ph /\ x e. R ) -> y e. ( Base ` ( RngCatALTV ` U ) ) ) )
44 43 impcom 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> y e. ( Base ` ( RngCatALTV ` U ) ) )
45 44 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> y e. ( Base ` ( RngCatALTV ` U ) ) )
46 36 sseld 
 |-  ( ph -> ( z e. R -> z e. ( Base ` ( RngCatALTV ` U ) ) ) )
47 46 adantr 
 |-  ( ( ph /\ x e. R ) -> ( z e. R -> z e. ( Base ` ( RngCatALTV ` U ) ) ) )
48 47 adantld 
 |-  ( ( ph /\ x e. R ) -> ( ( y e. R /\ z e. R ) -> z e. ( Base ` ( RngCatALTV ` U ) ) ) )
49 48 imp 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> z e. ( Base ` ( RngCatALTV ` U ) ) )
50 49 adantr 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> z e. ( Base ` ( RngCatALTV ` U ) ) )
51 rhmisrnghm 
 |-  ( f e. ( x RingHom y ) -> f e. ( x RngHomo y ) )
52 13 51 syl6bi 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( f e. ( x H y ) -> f e. ( x RngHomo y ) ) )
53 52 com12 
 |-  ( f e. ( x H y ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> f e. ( x RngHomo y ) ) )
54 53 adantr 
 |-  ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> f e. ( x RngHomo y ) ) )
55 54 impcom 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> f e. ( x RngHomo y ) )
56 rhmisrnghm 
 |-  ( g e. ( y RingHom z ) -> g e. ( y RngHomo z ) )
57 18 56 syl6bi 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( g e. ( y H z ) -> g e. ( y RngHomo z ) ) )
58 57 adantld 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) -> g e. ( y RngHomo z ) ) )
59 58 imp 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> g e. ( y RngHomo z ) )
60 24 25 26 27 39 45 50 55 59 rngccoALTV 
 |-  ( ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. ( comp ` ( RngCatALTV ` U ) ) z ) f ) = ( g o. f ) )
61 1 2 3 4 rhmsubcALTVlem2 
 |-  ( ( ph /\ x e. R /\ z e. R ) -> ( x H z ) = ( x RingHom z ) )
62 6 8 15 61 syl3anc 
 |-  ( ( ( ph /\ x e. R ) /\ ( y e. R /\ z e. R ) ) -> ( x H z ) = ( x RingHom z ) )
63 62 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 ) )
64 23 60 63 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 ` ( RngCatALTV ` U ) ) z ) f ) e. ( x H z ) )