This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngcco

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
rngcco.x ⊢ φ → X ∈ U
rngcco.y ⊢ φ → Y ∈ U
rngcco.z ⊢ φ → Z ∈ U
rngcco.f ⊢ φ → F : Base X ⟶ Base Y
rngcco.g ⊢ φ → G : Base Y ⟶ Base Z
Assertion rngcco ⊢ φ → G X Y · ˙ Z F = G ∘ F

Proof

Step Hyp Ref Expression
1 rngcco.c ⊢ C = RngCat ⁡ U
2 rngcco.u ⊢ φ → U ∈ V
3 rngcco.o ⊢ · ˙ = comp ⁡ C
4 rngcco.x ⊢ φ → X ∈ U
5 rngcco.y ⊢ φ → Y ∈ U
6 rngcco.z ⊢ φ → Z ∈ U
7 rngcco.f ⊢ φ → F : Base X ⟶ Base Y
8 rngcco.g ⊢ φ → G : Base Y ⟶ Base Z
9 1 2 3 rngccofval ⊢ φ → · ˙ = comp ⁡ ExtStrCat ⁡ U
10 9 oveqd ⊢ φ → X Y · ˙ Z = X Y comp ⁡ ExtStrCat ⁡ U Z
11 10 oveqd ⊢ φ → G X Y · ˙ Z F = G X Y comp ⁡ ExtStrCat ⁡ U Z F
12 eqid ⊢ ExtStrCat ⁡ U = ExtStrCat ⁡ U
13 eqid ⊢ comp ⁡ ExtStrCat ⁡ U = comp ⁡ ExtStrCat ⁡ U
14 eqid ⊢ Base X = Base X
15 eqid ⊢ Base Y = Base Y
16 eqid ⊢ Base Z = Base Z
17 12 2 13 4 5 6 14 15 16 7 8 estrcco ⊢ φ → G X Y comp ⁡ ExtStrCat ⁡ U Z F = G ∘ F
18 11 17 eqtrd ⊢ φ → G X Y · ˙ Z F = G ∘ F