Metamath Proof Explorer


Theorem rhmsscmap

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

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

Proof

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