Metamath Proof Explorer


Theorem rnghmsscmap2

Description: The non-unital ring homomorphisms between non-unital rings (in a universe) are a subcategory subset of the mappings between base sets of non-unital rings (in the same universe). (Contributed by AV, 6-Mar-2020)

Ref Expression
Hypotheses rnghmsscmap.u ( 𝜑𝑈𝑉 )
rnghmsscmap.r ( 𝜑𝑅 = ( Rng ∩ 𝑈 ) )
Assertion rnghmsscmap2 ( 𝜑 → ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 rnghmsscmap.u ( 𝜑𝑈𝑉 )
2 rnghmsscmap.r ( 𝜑𝑅 = ( Rng ∩ 𝑈 ) )
3 ssidd ( 𝜑𝑅𝑅 )
4 eqid ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
5 eqid ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
6 4 5 rnghmf ( ∈ ( 𝑎 RngHomo 𝑏 ) → : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) )
7 simpr ( ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) )
8 fvex ( Base ‘ 𝑏 ) ∈ V
9 fvex ( Base ‘ 𝑎 ) ∈ V
10 8 9 pm3.2i ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V )
11 elmapg ( ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) → ( ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
12 10 11 mp1i ( ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ( ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ↔ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
13 7 12 mpbird ( ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) ∧ : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) → ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
14 13 ex ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) → ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
15 6 14 syl5 ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( ∈ ( 𝑎 RngHomo 𝑏 ) → ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
16 15 ssrdv ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( 𝑎 RngHomo 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
17 ovres ( ( 𝑎𝑅𝑏𝑅 ) → ( 𝑎 ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 RngHomo 𝑏 ) )
18 17 adantl ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( 𝑎 ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 RngHomo 𝑏 ) )
19 eqidd ( ( 𝑎𝑅𝑏𝑅 ) → ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
20 fveq2 ( 𝑦 = 𝑏 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑏 ) )
21 fveq2 ( 𝑥 = 𝑎 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑎 ) )
22 20 21 oveqan12rd ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
23 22 adantl ( ( ( 𝑎𝑅𝑏𝑅 ) ∧ ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
24 simpl ( ( 𝑎𝑅𝑏𝑅 ) → 𝑎𝑅 )
25 simpr ( ( 𝑎𝑅𝑏𝑅 ) → 𝑏𝑅 )
26 ovexd ( ( 𝑎𝑅𝑏𝑅 ) → ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ∈ V )
27 19 23 24 25 26 ovmpod ( ( 𝑎𝑅𝑏𝑅 ) → ( 𝑎 ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
28 27 adantl ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( 𝑎 ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) = ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
29 16 18 28 3sstr4d ( ( 𝜑 ∧ ( 𝑎𝑅𝑏𝑅 ) ) → ( 𝑎 ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) )
30 29 ralrimivva ( 𝜑 → ∀ 𝑎𝑅𝑏𝑅 ( 𝑎 ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) )
31 rnghmfn RngHomo Fn ( Rng × Rng )
32 31 a1i ( 𝜑 → RngHomo Fn ( Rng × Rng ) )
33 inss1 ( Rng ∩ 𝑈 ) ⊆ Rng
34 2 33 eqsstrdi ( 𝜑𝑅 ⊆ Rng )
35 xpss12 ( ( 𝑅 ⊆ Rng ∧ 𝑅 ⊆ Rng ) → ( 𝑅 × 𝑅 ) ⊆ ( Rng × Rng ) )
36 34 34 35 syl2anc ( 𝜑 → ( 𝑅 × 𝑅 ) ⊆ ( Rng × Rng ) )
37 fnssres ( ( RngHomo Fn ( Rng × Rng ) ∧ ( 𝑅 × 𝑅 ) ⊆ ( Rng × Rng ) ) → ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
38 32 36 37 syl2anc ( 𝜑 → ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
39 eqid ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
40 ovex ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ∈ V
41 39 40 fnmpoi ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑅 × 𝑅 )
42 41 a1i ( 𝜑 → ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) Fn ( 𝑅 × 𝑅 ) )
43 incom ( Rng ∩ 𝑈 ) = ( 𝑈 ∩ Rng )
44 inex1g ( 𝑈𝑉 → ( 𝑈 ∩ Rng ) ∈ V )
45 1 44 syl ( 𝜑 → ( 𝑈 ∩ Rng ) ∈ V )
46 43 45 eqeltrid ( 𝜑 → ( Rng ∩ 𝑈 ) ∈ V )
47 2 46 eqeltrd ( 𝜑𝑅 ∈ V )
48 38 42 47 isssc ( 𝜑 → ( ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↔ ( 𝑅𝑅 ∧ ∀ 𝑎𝑅𝑏𝑅 ( 𝑎 ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) ) ) )
49 3 30 48 mpbir2and ( 𝜑 → ( RngHomo ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( 𝑥𝑅 , 𝑦𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )