Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspsn Structured version   Unicode version

Theorem rspsn 18112
 Description: Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
rspsn.b
rspsn.k RSpan
rspsn.d r
Assertion
Ref Expression
rspsn
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem rspsn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqcom 2409 . . . . 5
21a1i 11 . . . 4
32rexbidv 2915 . . 3
4 rlmlmod 18061 . . . 4 ringLMod
5 rlmsca2 18057 . . . . 5 ScalarringLMod
6 baseid 14779 . . . . . 6 Slot
7 rspsn.b . . . . . 6
86, 7strfvi 14773 . . . . 5
9 rlmbas 18051 . . . . . 6 ringLMod
107, 9eqtri 2429 . . . . 5 ringLMod
11 rlmvsca 18058 . . . . 5 ringLMod
12 rspsn.k . . . . . 6 RSpan
13 rspval 18049 . . . . . 6 RSpan ringLMod
1412, 13eqtri 2429 . . . . 5 ringLMod
155, 8, 10, 11, 14lspsnel 17859 . . . 4 ringLMod
164, 15sylan 469 . . 3
17 rspsn.d . . . . 5 r
18 eqid 2400 . . . . 5
197, 17, 18dvdsr2 17506 . . . 4