Theorem rspsn

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)

	Ref	Expression
Hypotheses	rspsn.b	|- B = ( Base ` R )
	rspsn.k	|- K = ( RSpan ` R )
	rspsn.d	|- .|| = ( ||r ` R )
Assertion	rspsn	|- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )

Proof

Step	Hyp	Ref	Expression
1		rspsn.b	|- B = ( Base ` R )
2		rspsn.k	|- K = ( RSpan ` R )
3		rspsn.d	|- .|| = ( ||r ` R )
4		eqcom	|- ( x = ( a ( .r ` R ) G ) <-> ( a ( .r ` R ) G ) = x )
5	4	a1i	|- ( ( R e. Ring /\ G e. B ) -> ( x = ( a ( .r ` R ) G ) <-> ( a ( .r ` R ) G ) = x ) )
6	5	rexbidv	|- ( ( R e. Ring /\ G e. B ) -> ( E. a e. B x = ( a ( .r ` R ) G ) <-> E. a e. B ( a ( .r ` R ) G ) = x ) )
7		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
8		rlmsca2	|- ( _I ` R ) = ( Scalar ` ( ringLMod ` R ) )
9		baseid	|- Base = Slot ( Base ` ndx )
10	9 1	strfvi	|- B = ( Base ` ( _I ` R ) )
11		rlmbas	|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
12	1 11	eqtri	|- B = ( Base ` ( ringLMod ` R ) )
13		rlmvsca	|- ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
14		rspval	|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
15	2 14	eqtri	|- K = ( LSpan ` ( ringLMod ` R ) )
16	8 10 12 13 15	lspsnel	|- ( ( ( ringLMod ` R ) e. LMod /\ G e. B ) -> ( x e. ( K ` { G } ) <-> E. a e. B x = ( a ( .r ` R ) G ) ) )
17	7 16	sylan	|- ( ( R e. Ring /\ G e. B ) -> ( x e. ( K ` { G } ) <-> E. a e. B x = ( a ( .r ` R ) G ) ) )
18		eqid	|- ( .r ` R ) = ( .r ` R )
19	1 3 18	dvdsr2	|- ( G e. B -> ( G .|| x <-> E. a e. B ( a ( .r ` R ) G ) = x ) )
20	19	adantl	|- ( ( R e. Ring /\ G e. B ) -> ( G .|| x <-> E. a e. B ( a ( .r ` R ) G ) = x ) )
21	6 17 20	3bitr4d	|- ( ( R e. Ring /\ G e. B ) -> ( x e. ( K ` { G } ) <-> G .|| x ) )
22	21	abbi2dv	|- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )