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

Metamath Proof Explorer

Theorem ringcco

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

Ref Expression
Hypotheses ringcco.c ⊢ C = RingCat ⁡ U
ringcco.u ⊢ φ → U ∈ V
ringcco.o ⊢ · ˙ = comp ⁡ C
ringcco.x ⊢ φ → X ∈ U
ringcco.y ⊢ φ → Y ∈ U
ringcco.z ⊢ φ → Z ∈ U
ringcco.f ⊢ φ → F : Base X ⟶ Base Y
ringcco.g ⊢ φ → G : Base Y ⟶ Base Z
Assertion ringcco ⊢ φ → G X Y · ˙ Z F = G ∘ F

Proof

Step Hyp Ref Expression
1 ringcco.c ⊢ C = RingCat ⁡ U
2 ringcco.u ⊢ φ → U ∈ V
3 ringcco.o ⊢ · ˙ = comp ⁡ C
4 ringcco.x ⊢ φ → X ∈ U
5 ringcco.y ⊢ φ → Y ∈ U
6 ringcco.z ⊢ φ → Z ∈ U
7 ringcco.f ⊢ φ → F : Base X ⟶ Base Y
8 ringcco.g ⊢ φ → G : Base Y ⟶ Base Z
9 1 2 3 ringccofval ⊢ φ → · ˙ = 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