Metamath Proof Explorer


Theorem rhmsubclem3

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

Ref Expression
Hypotheses rngcrescrhm.u φ U V
rngcrescrhm.c C = RngCat U
rngcrescrhm.r φ R = Ring U
rngcrescrhm.h H = RingHom R × R
Assertion rhmsubclem3 φ x R Id RngCat U x x H x

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u φ U V
2 rngcrescrhm.c C = RngCat U
3 rngcrescrhm.r φ R = Ring U
4 rngcrescrhm.h H = RingHom R × R
5 3 eleq2d φ x R x Ring U
6 elinel1 x Ring U x Ring
7 5 6 syl6bi φ x R x Ring
8 7 imp φ x R x Ring
9 eqid Base x = Base x
10 9 idrhm x Ring I Base x x RingHom x
11 8 10 syl φ x R I Base x x RingHom x
12 eqid Base C = Base C
13 2 eqcomi RngCat U = C
14 13 fveq2i Id RngCat U = Id C
15 1 adantr φ x R U V
16 incom Ring U = U Ring
17 ringssrng Ring Rng
18 sslin Ring Rng U Ring U Rng
19 17 18 mp1i φ U Ring U Rng
20 16 19 eqsstrid φ Ring U U Rng
21 2 12 1 rngcbas φ Base C = U Rng
22 20 3 21 3sstr4d φ R Base C
23 22 sselda φ x R x Base C
24 2 12 14 15 23 9 rngcid φ x R Id RngCat U x = I Base x
25 1 2 3 4 rhmsubclem2 φ x R x R x H x = x RingHom x
26 25 3anidm23 φ x R x H x = x RingHom x
27 11 24 26 3eltr4d φ x R Id RngCat U x x H x