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	ellspsn	\|- ( ( ( 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	eqabdv	\|- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x \| G .\|\| x } )

Metamath Proof Explorer

Theorem rspsn

Proof