Metamath Proof Explorer


Theorem rngccofval

Description: Composition in the category of non-unital rings. (Contributed by AV, 27-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses rngcco.c C = RngCat U
rngcco.u φ U V
rngcco.o · ˙ = comp C
Assertion rngccofval φ · ˙ = comp ExtStrCat U

Proof

Step Hyp Ref Expression
1 rngcco.c C = RngCat U
2 rngcco.u φ U V
3 rngcco.o · ˙ = comp C
4 eqid Base C = Base C
5 1 4 2 rngcbas φ Base C = U Rng
6 eqid Hom C = Hom C
7 1 4 2 6 rngchomfval φ Hom C = RngHomo Base C × Base C
8 1 2 5 7 rngcval φ C = ExtStrCat U cat Hom C
9 8 fveq2d φ comp C = comp ExtStrCat U cat Hom C
10 3 a1i φ · ˙ = comp C
11 eqid ExtStrCat U cat Hom C = ExtStrCat U cat Hom C
12 eqid Base ExtStrCat U = Base ExtStrCat U
13 fvexd φ ExtStrCat U V
14 5 7 rnghmresfn φ Hom C Fn Base C × Base C
15 inss1 U Rng U
16 15 a1i φ U Rng U
17 eqid ExtStrCat U = ExtStrCat U
18 17 2 estrcbas φ U = Base ExtStrCat U
19 18 eqcomd φ Base ExtStrCat U = U
20 16 5 19 3sstr4d φ Base C Base ExtStrCat U
21 eqid comp ExtStrCat U = comp ExtStrCat U
22 11 12 13 14 20 21 rescco φ comp ExtStrCat U = comp ExtStrCat U cat Hom C
23 9 10 22 3eqtr4d φ · ˙ = comp ExtStrCat U