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

Metamath Proof Explorer

Theorem ringcval

Description: Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcval.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
ringcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
ringcval.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
ringcval.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion ringcval ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ringcval.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
2 ringcval.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3 ringcval.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
4 ringcval.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5 df-ringc ⊢ RingCat = ( 𝑢 ∈ V ↦ ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) ) )
6 fveq2 ⊢ ( 𝑢 = 𝑈 → ( ExtStrCat ‘ 𝑢 ) = ( ExtStrCat ‘ 𝑈 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ExtStrCat ‘ 𝑢 ) = ( ExtStrCat ‘ 𝑈 ) )
8 ineq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∩ Ring ) = ( 𝑈 ∩ Ring ) )
9 8 sqxpeqd ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) = ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) )
10 3 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) )
11 10 eqcomd ⊢ ( 𝜑 → ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) = ( 𝐵 × 𝐵 ) )
12 9 11 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) = ( 𝐵 × 𝐵 ) )
13 12 reseq2d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
14 4 eqcomd ⊢ ( 𝜑 → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 )
16 13 15 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) = 𝐻 )
17 7 16 oveq12d ⊢ ( ( 𝜑 ∧ 𝑢 = 𝑈 ) → ( ( ExtStrCat ‘ 𝑢 ) ↾cat ( RingHom ↾ ( ( 𝑢 ∩ Ring ) × ( 𝑢 ∩ Ring ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) )
18 2 elexd ⊢ ( 𝜑 → 𝑈 ∈ V )
19 ovexd ⊢ ( 𝜑 → ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) ∈ V )
20 5 17 18 19 fvmptd2 ⊢ ( 𝜑 → ( RingCat ‘ 𝑈 ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) )
21 1 20 eqtrid ⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) )