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 ‘ 𝑥 ) ) ) )