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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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 ‘ 𝑅 ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
13 7 4 10 12 rnghmsubcsetc ⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
14 13 idi ⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
15 eqid ⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) )
16 eqid ⊢ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) )
17 1 4 8 12 rngcval ⊢ ( 𝜑 → 𝑅 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) )
18 17 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
19 3 18 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
20 19 reseq2d ⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( I ↾ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ) )
21 5 20 eqtrd ⊢ ( 𝜑 → 𝐹 = ( I ↾ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ) )
22 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) )
23 12 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) )
24 ovres ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 RngHomo 𝑦 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 RngHomo 𝑦 ) )
26 23 25 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 RngHomo 𝑦 ) = ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) )
27 26 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) )
28 19 22 27 mpoeq123dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) , 𝑦 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) ) )
29 6 28 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) , 𝑦 ∈ ( Base ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) ) ↦ ( I ↾ ( 𝑥 ( Hom ‘ 𝑅 ) 𝑦 ) ) ) )
30 14 15 16 21 29 inclfusubc ⊢ ( 𝜑 → 𝐹 ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) 𝐺 )
31 2 a1i ⊢ ( 𝜑 → 𝐸 = ( ExtStrCat ‘ 𝑈 ) )
32 17 31 oveq12d ⊢ ( 𝜑 → ( 𝑅 Func 𝐸 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) )
33 32 breqd ⊢ ( 𝜑 → ( 𝐹 ( 𝑅 Func 𝐸 ) 𝐺 ↔ 𝐹 ( ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( Hom ‘ 𝑅 ) ) Func ( ExtStrCat ‘ 𝑈 ) ) 𝐺 ) )
34 30 33 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝐸 ) 𝐺 )