Theorem rnghmsscmap2 41765

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

Hypotheses

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

Assertion

Ref	Expression
rnghmsscmap2	⊢ (𝜑 → ( RngHomo ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))

Distinct variable group:   𝑥,𝑅,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem rnghmsscmap2

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

Step	Hyp	Ref	Expression
1		ssid 3587	. . 3 ⊢ 𝑅 ⊆ 𝑅
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝑅 ⊆ 𝑅)
3		eqid 2610	. . . . . . 7 ⊢ (Base‘𝑎) = (Base‘𝑎)
4		eqid 2610	. . . . . . 7 ⊢ (Base‘𝑏) = (Base‘𝑏)
5	3, 4	rnghmf 41689	. . . . . 6 ⊢ (ℎ ∈ (𝑎 RngHomo 𝑏) → ℎ:(Base‘𝑎)⟶(Base‘𝑏))
6		simpr 476	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ:(Base‘𝑎)⟶(Base‘𝑏))
7		fvex 6113	. . . . . . . . . 10 ⊢ (Base‘𝑏) ∈ V
8		fvex 6113	. . . . . . . . . 10 ⊢ (Base‘𝑎) ∈ V
9	7, 8	pm3.2i 470	. . . . . . . . 9 ⊢ ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)
10		elmapg 7757	. . . . . . . . 9 ⊢ (((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V) → (ℎ ∈ ((Base‘𝑏) ↑𝑚 (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏)))
11	9, 10	mp1i 13	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → (ℎ ∈ ((Base‘𝑏) ↑𝑚 (Base‘𝑎)) ↔ ℎ:(Base‘𝑎)⟶(Base‘𝑏)))
12	6, 11	mpbird 246	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) ∧ ℎ:(Base‘𝑎)⟶(Base‘𝑏)) → ℎ ∈ ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
13	12	ex 449	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ:(Base‘𝑎)⟶(Base‘𝑏) → ℎ ∈ ((Base‘𝑏) ↑𝑚 (Base‘𝑎))))
14	5, 13	syl5 33	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (ℎ ∈ (𝑎 RngHomo 𝑏) → ℎ ∈ ((Base‘𝑏) ↑𝑚 (Base‘𝑎))))
15	14	ssrdv 3574	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎 RngHomo 𝑏) ⊆ ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
16		ovres 6698	. . . . 5 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝑎( RngHomo ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RngHomo 𝑏))
17	16	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RngHomo ↾ (𝑅 × 𝑅))𝑏) = (𝑎 RngHomo 𝑏))
18		eqidd 2611	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) = (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))
19		fveq2 6103	. . . . . . . 8 ⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏))
20		fveq2 6103	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎))
21	19, 20	oveqan12rd 6569	. . . . . . 7 ⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) = ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
22	21	adantl 481	. . . . . 6 ⊢ (((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) = ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
23		simpl 472	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → 𝑎 ∈ 𝑅)
24		simpr 476	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → 𝑏 ∈ 𝑅)
25		ovex 6577	. . . . . . 7 ⊢ ((Base‘𝑏) ↑𝑚 (Base‘𝑎)) ∈ V
26	25	a1i 11	. . . . . 6 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → ((Base‘𝑏) ↑𝑚 (Base‘𝑎)) ∈ V)
27	18, 22, 23, 24, 26	ovmpt2d 6686	. . . . 5 ⊢ ((𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅) → (𝑎(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))𝑏) = ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
28	27	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))𝑏) = ((Base‘𝑏) ↑𝑚 (Base‘𝑎)))
29	15, 17, 28	3sstr4d 3611	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑅 ∧ 𝑏 ∈ 𝑅)) → (𝑎( RngHomo ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))𝑏))
30	29	ralrimivva 2954	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RngHomo ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))𝑏))
31		rnghmfn 41680	. . . . 5 ⊢ RngHomo Fn (Rng × Rng)
32	31	a1i 11	. . . 4 ⊢ (𝜑 → RngHomo Fn (Rng × Rng))
33		rnghmsscmap.r	. . . . . 6 ⊢ (𝜑 → 𝑅 = (Rng ∩ 𝑈))
34		inss1 3795	. . . . . 6 ⊢ (Rng ∩ 𝑈) ⊆ Rng
35	33, 34	syl6eqss 3618	. . . . 5 ⊢ (𝜑 → 𝑅 ⊆ Rng)
36		xpss12 5148	. . . . 5 ⊢ ((𝑅 ⊆ Rng ∧ 𝑅 ⊆ Rng) → (𝑅 × 𝑅) ⊆ (Rng × Rng))
37	35, 35, 36	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝑅 × 𝑅) ⊆ (Rng × Rng))
38		fnssres 5918	. . . 4 ⊢ (( RngHomo Fn (Rng × Rng) ∧ (𝑅 × 𝑅) ⊆ (Rng × Rng)) → ( RngHomo ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅))
39	32, 37, 38	syl2anc 691	. . 3 ⊢ (𝜑 → ( RngHomo ↾ (𝑅 × 𝑅)) Fn (𝑅 × 𝑅))
40		eqid 2610	. . . . 5 ⊢ (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) = (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))
41		ovex 6577	. . . . 5 ⊢ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) ∈ V
42	40, 41	fnmpt2i 7128	. . . 4 ⊢ (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) Fn (𝑅 × 𝑅)
43	42	a1i 11	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) Fn (𝑅 × 𝑅))
44		incom 3767	. . . . 5 ⊢ (Rng ∩ 𝑈) = (𝑈 ∩ Rng)
45		rnghmsscmap.u	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
46		inex1g 4729	. . . . . 6 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∩ Rng) ∈ V)
47	45, 46	syl 17	. . . . 5 ⊢ (𝜑 → (𝑈 ∩ Rng) ∈ V)
48	44, 47	syl5eqel 2692	. . . 4 ⊢ (𝜑 → (Rng ∩ 𝑈) ∈ V)
49	33, 48	eqeltrd 2688	. . 3 ⊢ (𝜑 → 𝑅 ∈ V)
50	39, 43, 49	isssc 16303	. 2 ⊢ (𝜑 → (( RngHomo ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ↔ (𝑅 ⊆ 𝑅 ∧ ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑅 (𝑎( RngHomo ↾ (𝑅 × 𝑅))𝑏) ⊆ (𝑎(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))𝑏))))
51	2, 30, 50	mpbir2and 959	1 ⊢ (𝜑 → ( RngHomo ↾ (𝑅 × 𝑅)) ⊆cat (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑅 ↦ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   class class class wbr 4583   × cxp 5036   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑_𝑚 cmap 7744  Basecbs 15695   ⊆_cat cssc 16290  Rngcrng 41664   RngHomo crngh 41675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-ixp 7795  df-ssc 16293  df-ghm 17481  df-abl 18019  df-rng0 41665  df-rnghomo 41677

This theorem is referenced by: (None)