Theorem rhmsscmap 20821

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.)

Hypotheses

Ref	Expression
rhmsscmap.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
rhmsscmap.r	⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))

Assertion

Ref	Expression
rhmsscmap	⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))

Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑉(𝑥, 𝑦)

Proof of Theorem rhmsscmap

Dummy variables 𝑎 𝑏 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rhmsscmap.r	. . 3 ⊢ (𝜑 → 𝑅 = (Ring ∩ 𝑈))
2		inss2 4183	. . 3 ⊢ (Ring ∩ 𝑈) ⊆ 𝑈
3	1, 2	eqsstrdi 3975	. 2 ⊢ (𝜑 → 𝑅 ⊆ 𝑈)
4		eqid 2760	. . . . . . 7 ⊢ (Base‘𝑎) = (Base‘𝑎)
5		eqid 2760	. . . . . . 7 ⊢ (Base‘𝑏) = (Base‘𝑏)
6	4, 5	rhmf 20626	. . . . . 6 ⊢ (ℎ ∈ (𝑎 RingHom 𝑏) → ℎ:(Base‘𝑎)⟶(Base‘𝑏))
7		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ:(Base‘𝑎)⟶(Base‘𝑏))
8		fvex 6891	. . . . . . . . . 10 ⊢ (Base‘𝑏) ∈ V
9		fvex 6891	. . . . . . . . . 10 ⊢ (Base‘𝑎) ∈ V
10	8, 9	pm3.2i 476	. . . . . . . . 9 ⊢ ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)
11		elmapg 8838	. . . . . . . . 9 ⊢ (((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V) → (ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏)))
12	10, 11	mp1i 14	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → (ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏)))
13	7, 12	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎)))
14	13	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ:(Base‘𝑎)⟶(Base‘𝑏) → ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎))))
15	6, 14	syl5 35	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ ∈ (𝑎 RingHom 𝑏) → ℎ ∈ ((Base‘𝑏) ↑m (Base‘𝑎))))
16	15	ssrdv 3937	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎 RingHom 𝑏) ⊆ ((Base‘𝑏) ↑m (Base‘𝑎)))
17		ovres 7579	. . . . 5 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RingHom 𝑏))
18	17	adantl 487	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RingHom 𝑏))
19		eqidd 2761	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))
20		fveq2 6878	. . . . . . 7 ⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏))
21		fveq2 6878	. . . . . . 7 ⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎))
22	20, 21	oveqan12rd 7433	. . . . . 6 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑏) ↑m (Base‘𝑎)))
23	22	adantl 487	. . . . 5 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑏) ↑m (Base‘𝑎)))
24	3	sseld 3930	. . . . . . . 8 ⊢ (𝜑 → (𝑎 ∈ 𝑅 → 𝑎 ∈ 𝑈))
25	24	com12 33	. . . . . . 7 ⊢ (𝑎 ∈ 𝑅 → (𝜑 → 𝑎 ∈ 𝑈))
26	25	adantr 486	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝜑 → 𝑎 ∈ 𝑈))
27	26	impcom 413	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → 𝑎 ∈ 𝑈)
28	3	sseld 3930	. . . . . . . 8 ⊢ (𝜑 → (𝑏 ∈ 𝑅 → 𝑏 ∈ 𝑈))
29	28	com12 33	. . . . . . 7 ⊢ (𝑏 ∈ 𝑅 → (𝜑 → 𝑏 ∈ 𝑈))
30	29	adantl 487	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝜑 → 𝑏 ∈ 𝑈))
31	30	impcom 413	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → 𝑏 ∈ 𝑈)
32		ovexd 7448	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → ((Base‘𝑏) ↑m (Base‘𝑎)) ∈ V)
33	19, 23, 27, 31, 32	ovmpod 7565	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))𝑏) = ((Base‘𝑏) ↑m (Base‘𝑎)))
34	16, 18, 33	3sstr4d 3986	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))𝑏))
35	34	ralrimivva 3205	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))𝑏))
36		rhmfn 20647	. . . . 5 ⊢ RingHom Fn (Ring × Ring)
37	36	a1i 11	. . . 4 ⊢ (𝜑 → RingHom Fn (Ring × Ring))
38		inss1 4182	. . . . . 6 ⊢ (Ring ∩ 𝑈) ⊆ Ring
39	1, 38	eqsstrdi 3975	. . . . 5 ⊢ (𝜑 → 𝑅 ⊆ Ring)
40		xpss12 5670	. . . . 5 ⊢ ((𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring) → (𝑅 × 𝑅) ⊆ (Ring × Ring))
41	39, 39, 40	syl2anc 596	. . . 4 ⊢ (𝜑 → (𝑅 × 𝑅) ⊆ (Ring × Ring))
42		fnssres 6655	. . . 4 ⊢ (( RingHom Fn (Ring × Ring) ∧ (𝑅 × 𝑅) ⊆ (Ring × Ring)) → ( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅))
43	37, 41, 42	syl2anc 596	. . 3 ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅))
44		eqid 2760	. . . . 5 ⊢ (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))
45		ovex 7446	. . . . 5 ⊢ ((Base‘𝑦) ↑m (Base‘𝑥)) ∈ V
46	44, 45	fnmpoi 8067	. . . 4 ⊢ (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) Fn (𝑈 × 𝑈)
47	46	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) Fn (𝑈 × 𝑈))
48		rhmsscmap.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
49		elex 3471	. . . 4 ⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ V)
50	48, 49	syl 18	. . 3 ⊢ (𝜑 → 𝑈 ∈ V)
51	43, 47, 50	isssc 17909	. 2 ⊢ (𝜑 → (( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))) ↔ (𝑅 ⊆ 𝑈 ∧ ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RingHom ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))𝑏))))
52	3, 35, 51	mpbir2and 726	1 ⊢ (𝜑 → ( RingHom ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ((Base‘𝑦) ↑m (Base‘𝑥))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ∩ cin 3898   ⊆ wss 3899   class class class wbr 5103   × cxp 5653   ↾ cres 5657   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413   ∈ cmpo 7415   ↑_m cmap 8826  Basecbs 17301   ⊆_cat cssc 17896  Ringcrg 20372   RingHom crh 20610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-map 8828  df-ixp 8905  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-plusg 17355  df-0g 17526  df-ssc 17899  df-mhm 18891  df-ghm 19341  df-mgp 20274  df-ur 20321  df-ring 20374  df-rhm 20613

This theorem is used by:  rhmsubcsetc  20824