Metamath Proof Explorer

Theorem rhmsscmap2

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

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

Proof

Step Hyp Ref Expression
1 rhmsscmap.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rhmsscmap.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
3 ssidd ⊢ ( 𝜑 → 𝑅 ⊆ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
5 eqid ⊢ ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
6 4 5 rhmf ⊢ ( ℎ ∈ ( 𝑎 RingHom 𝑏 ) → ℎ : ( 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 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅 ) ) → ( ℎ ∈ ( 𝑎 RingHom 𝑏 ) → ℎ ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
16 15 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅 ) ) → ( 𝑎 RingHom 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
17 ovres ⊢ ( ( 𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅 ) → ( 𝑎 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 RingHom 𝑏 ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅 ) ) → ( 𝑎 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) = ( 𝑎 RingHom 𝑏 ) )
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 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅 ) ) → ( 𝑎 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) )
30 29 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑅 ∀ 𝑏 ∈ 𝑅 ( 𝑎 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) )
31 rhmfn ⊢ RingHom Fn ( Ring × Ring )
32 31 a1i ⊢ ( 𝜑 → RingHom Fn ( Ring × Ring ) )
33 inss1 ⊢ ( Ring ∩ 𝑈 ) ⊆ Ring
34 2 33 eqsstrdi ⊢ ( 𝜑 → 𝑅 ⊆ Ring )
35 xpss12 ⊢ ( ( 𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring ) → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
36 34 34 35 syl2anc ⊢ ( 𝜑 → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
37 fnssres ⊢ ( ( RingHom Fn ( Ring × Ring ) ∧ ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) ) → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
38 32 36 37 syl2anc ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 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 ⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
44 inex1g ⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) ∈ V )
45 1 44 syl ⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ∈ V )
46 43 45 eqeltrid ⊢ ( 𝜑 → ( Ring ∩ 𝑈 ) ∈ V )
47 2 46 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ V )
48 38 42 47 isssc ⊢ ( 𝜑 → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↔ ( 𝑅 ⊆ 𝑅 ∧ ∀ 𝑎 ∈ 𝑅 ∀ 𝑏 ∈ 𝑅 ( 𝑎 ( RingHom ↾ ( 𝑅 × 𝑅 ) ) 𝑏 ) ⊆ ( 𝑎 ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) 𝑏 ) ) ) )
49 3 30 48 mpbir2and ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) ⊆cat ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )