Theorem subrgdvds 13361

Description: If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)

Hypotheses

Ref	Expression
subrgdvds.1	⊢ 𝑆 = (𝑅 ↾s 𝐴)
subrgdvds.2	⊢ ∥ = (∥r‘𝑅)
subrgdvds.3	⊢ 𝐸 = (∥r‘𝑆)

Assertion

Ref	Expression
subrgdvds	⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ )

Proof of Theorem subrgdvds

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		subrgdvds.1	. . . . 5 ⊢ 𝑆 = (𝑅 ↾s 𝐴)
2	1	subrgring 13350	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ Ring)
3		ringsrg 13229	. . . 4 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ SRing)
4	2, 3	syl 14	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑆 ∈ SRing)
5		reldvdsrsrg 13266	. . . 4 ⊢ (𝑆 ∈ SRing → Rel (∥r‘𝑆))
6		subrgdvds.3	. . . . 5 ⊢ 𝐸 = (∥r‘𝑆)
7	6	releqi 4711	. . . 4 ⊢ (Rel 𝐸 ↔ Rel (∥r‘𝑆))
8	5, 7	sylibr 134	. . 3 ⊢ (𝑆 ∈ SRing → Rel 𝐸)
9	4, 8	syl 14	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → Rel 𝐸)
10	1	subrgbas 13356	. . . . . . 7 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆))
11		eqid 2177	. . . . . . . 8 ⊢ (Base‘𝑅) = (Base‘𝑅)
12	11	subrgss 13348	. . . . . . 7 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅))
13	10, 12	eqsstrrd 3194	. . . . . 6 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) ⊆ (Base‘𝑅))
14	13	sseld 3156	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥 ∈ (Base‘𝑆) → 𝑥 ∈ (Base‘𝑅)))
15		subrgrcl 13352	. . . . . . . . . 10 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring)
16		eqid 2177	. . . . . . . . . . 11 ⊢ (.r‘𝑅) = (.r‘𝑅)
17	1, 16	ressmulrg 12605	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑅 ∈ Ring) → (.r‘𝑅) = (.r‘𝑆))
18	15, 17	mpdan 421	. . . . . . . . 9 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (.r‘𝑅) = (.r‘𝑆))
19	18	oveqd 5894	. . . . . . . 8 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑧(.r‘𝑅)𝑥) = (𝑧(.r‘𝑆)𝑥))
20	19	eqeq1d 2186	. . . . . . 7 ⊢ (𝐴 ∈ (SubRing‘𝑅) → ((𝑧(.r‘𝑅)𝑥) = 𝑦 ↔ (𝑧(.r‘𝑆)𝑥) = 𝑦))
21	20	rexbidv 2478	. . . . . 6 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑅)𝑥) = 𝑦 ↔ ∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑆)𝑥) = 𝑦))
22		ssrexv 3222	. . . . . . 7 ⊢ ((Base‘𝑆) ⊆ (Base‘𝑅) → (∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑅)𝑥) = 𝑦 → ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦))
23	13, 22	syl 14	. . . . . 6 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑅)𝑥) = 𝑦 → ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦))
24	21, 23	sylbird 170	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑆)𝑥) = 𝑦 → ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦))
25	14, 24	anim12d 335	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) → ((𝑥 ∈ (Base‘𝑆) ∧ ∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑆)𝑥) = 𝑦) → (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)))
26		eqidd 2178	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) = (Base‘𝑆))
27	6	a1i 9	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 = (∥r‘𝑆))
28		eqidd 2178	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (.r‘𝑆) = (.r‘𝑆))
29	26, 27, 4, 28	dvdsrd 13268	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥𝐸𝑦 ↔ (𝑥 ∈ (Base‘𝑆) ∧ ∃𝑧 ∈ (Base‘𝑆)(𝑧(.r‘𝑆)𝑥) = 𝑦)))
30		eqidd 2178	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑅) = (Base‘𝑅))
31		subrgdvds.2	. . . . . 6 ⊢ ∥ = (∥r‘𝑅)
32	31	a1i 9	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → ∥ = (∥r‘𝑅))
33		ringsrg 13229	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing)
34	15, 33	syl 14	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ SRing)
35		eqidd 2178	. . . . 5 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (.r‘𝑅) = (.r‘𝑅))
36	30, 32, 34, 35	dvdsrd 13268	. . . 4 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥 ∥ 𝑦 ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)))
37	25, 29, 36	3imtr4d 203	. . 3 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥𝐸𝑦 → 𝑥 ∥ 𝑦))
38		df-br 4006	. . 3 ⊢ (𝑥𝐸𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐸)
39		df-br 4006	. . 3 ⊢ (𝑥 ∥ 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ ∥ )
40	37, 38, 39	3imtr3g 204	. 2 ⊢ (𝐴 ∈ (SubRing‘𝑅) → (⟨𝑥, 𝑦⟩ ∈ 𝐸 → ⟨𝑥, 𝑦⟩ ∈ ∥ ))
41	9, 40	relssdv 4720	1 ⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐸 ⊆ ∥ )

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  ∃wrex 2456   ⊆ wss 3131  ⟨cop 3597   class class class wbr 4005  Rel wrel 4633  ‘cfv 5218  (class class class)co 5877  Basecbs 12464   ↾_s cress 12465  ._rcmulr 12539  SRingcsrg 13151  Ringcrg 13184  ∥_rcdsr 13260  SubRingcsubrg 13343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-pre-ltirr 7925  ax-pre-lttrn 7927  ax-pre-ltadd 7929

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pnf 7996  df-mnf 7997  df-ltxr 7999  df-inn 8922  df-2 8980  df-3 8981  df-ndx 12467  df-slot 12468  df-base 12470  df-sets 12471  df-iress 12472  df-plusg 12551  df-mulr 12552  df-0g 12712  df-mgm 12780  df-sgrp 12813  df-mnd 12823  df-grp 12885  df-minusg 12886  df-subg 13035  df-cmn 13095  df-abl 13096  df-mgp 13136  df-ur 13148  df-srg 13152  df-ring 13186  df-dvdsr 13263  df-subrg 13345

This theorem is referenced by:  subrguss  13362