Metamath Proof Explorer


Theorem rhmsubcsetclem1

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

Ref Expression
Hypotheses rhmsubcsetc.c C = ExtStrCat U
rhmsubcsetc.u φ U V
rhmsubcsetc.b φ B = Ring U
rhmsubcsetc.h φ H = RingHom B × B
Assertion rhmsubcsetclem1 φ x B Id C x x H x

Proof

Step Hyp Ref Expression
1 rhmsubcsetc.c C = ExtStrCat U
2 rhmsubcsetc.u φ U V
3 rhmsubcsetc.b φ B = Ring U
4 rhmsubcsetc.h φ H = RingHom B × B
5 3 eleq2d φ x B x Ring U
6 elin x Ring U x Ring x U
7 6 simplbi x Ring U x Ring
8 5 7 syl6bi φ x B x Ring
9 8 imp φ x B x Ring
10 eqid Base x = Base x
11 10 idrhm x Ring I Base x x RingHom x
12 9 11 syl φ x B I Base x x RingHom x
13 eqid Id C = Id C
14 2 adantr φ x B U V
15 6 simprbi x Ring U x U
16 5 15 syl6bi φ x B x U
17 16 imp φ x B x U
18 1 13 14 17 estrcid φ x B Id C x = I Base x
19 4 oveqdr φ x B x H x = x RingHom B × B x
20 eqid RingCat U = RingCat U
21 eqid Base RingCat U = Base RingCat U
22 eqid Hom RingCat U = Hom RingCat U
23 20 21 2 22 ringchomfval φ Hom RingCat U = RingHom Base RingCat U × Base RingCat U
24 20 21 2 ringcbas φ Base RingCat U = U Ring
25 incom Ring U = U Ring
26 3 25 syl6eq φ B = U Ring
27 26 eqcomd φ U Ring = B
28 24 27 eqtrd φ Base RingCat U = B
29 28 sqxpeqd φ Base RingCat U × Base RingCat U = B × B
30 29 reseq2d φ RingHom Base RingCat U × Base RingCat U = RingHom B × B
31 23 30 eqtrd φ Hom RingCat U = RingHom B × B
32 31 adantr φ x B Hom RingCat U = RingHom B × B
33 32 eqcomd φ x B RingHom B × B = Hom RingCat U
34 33 oveqd φ x B x RingHom B × B x = x Hom RingCat U x
35 26 eleq2d φ x B x U Ring
36 35 biimpa φ x B x U Ring
37 24 adantr φ x B Base RingCat U = U Ring
38 36 37 eleqtrrd φ x B x Base RingCat U
39 20 21 14 22 38 38 ringchom φ x B x Hom RingCat U x = x RingHom x
40 19 34 39 3eqtrd φ x B x H x = x RingHom x
41 12 18 40 3eltr4d φ x B Id C x x H x