Metamath Proof Explorer

Theorem rngcifuestrc

Description: The "inclusion functor" from the category of non-unital rings into the category of extensible structures. (Contributed by AV, 30-Mar-2020)

Ref Expression
Hypotheses rngcifuestrc.r ⊢ 𝑅 = ( RngCat ‘ 𝑈 )
rngcifuestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
rngcifuestrc.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rngcifuestrc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcifuestrc.f ⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
rngcifuestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
Assertion rngcifuestrc ( 𝜑 → 𝐹 ( 𝑅 Func 𝐸 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 rngcifuestrc.r ⊢ 𝑅 = ( RngCat ‘ 𝑈 )
2 rngcifuestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
3 rngcifuestrc.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 rngcifuestrc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
5 rngcifuestrc.f ⊢ ( 𝜑 → 𝐹 = ( I ↾ 𝐵 ) )
6 rngcifuestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
7 eqid ⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
8 1 3 4 rngcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
9 incom ⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
10 8 9 eqtrdi ⊢ ( 𝜑 → 𝐵 = ( Rng ∩ 𝑈 ) )
11 eqid ⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
12 1 3 4 11 rngchomfval ⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) = ( RngHom ↾ ( 𝐵 × 𝐵 ) ) )
13 7 4 10 12 rnghmsubcsetc ⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
14 eqid ⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) )
15 eqid ⊢ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) )
16 1 4 8 12 rngcval ⊢ ( 𝜑 → 𝑅 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) )
17 16 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
18 3 17 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
19 18 reseq2d ⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( I ↾ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ) )
20 5 19 eqtrd ⊢ ( 𝜑 → 𝐹 = ( I ↾ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ) )
21 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
22 12 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( RngHom ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) )
23 ovres ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( RngHom ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 RngHom 𝑦 ) )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( RngHom ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 RngHom 𝑦 ) )
25 22 24 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 RngHom 𝑦 ) = ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) )
26 25 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHom 𝑦 ) ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) )
27 18 21 26 mpoeq123dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) , 𝑦 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) ) )
28 6 27 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) , 𝑦 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) ) )
29 13 14 15 20 28 inclfusubc ⊢ ( 𝜑 → 𝐹 ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) 𝐺 )
30 2 a1i ⊢ ( 𝜑 → 𝐸 = ( ExtStrCat ‘ 𝑈 ) )
31 16 30 oveq12d ⊢ ( 𝜑 → ( 𝑅 Func 𝐸 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) )
32 31 breqd ⊢ ( 𝜑 → ( 𝐹 ( 𝑅 Func 𝐸 ) 𝐺 ↔ 𝐹 ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) 𝐺 ) )
33 29 32 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝐸 ) 𝐺 )