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	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	rspsn	$⊢ (R \in Ring \land G \in B) \to K (\{G\}) = \{x \| G \underset{˙}{∥} x\}$

Proof

Step	Hyp	Ref	Expression
1		rspsn.b	$⊢ B = {Base}_{R}$
2		rspsn.k	$⊢ K = RSpan (R)$
3		rspsn.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		eqcom	$⊢ x = a \cdot_{R} G \leftrightarrow a \cdot_{R} G = x$
5	4	a1i	$⊢ (R \in Ring \land G \in B) \to (x = a \cdot_{R} G \leftrightarrow a \cdot_{R} G = x)$
6	5	rexbidv	$⊢ (R \in Ring \land G \in B) \to (\exists a \in B x = a \cdot_{R} G \leftrightarrow \exists a \in B a \cdot_{R} G = x)$
7		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in 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	$⊢ \cdot_{R} = \cdot_{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) \in LMod \land G \in B) \to (x \in K (\{G\}) \leftrightarrow \exists a \in B x = a \cdot_{R} G)$
17	7 16	sylan	$⊢ (R \in Ring \land G \in B) \to (x \in K (\{G\}) \leftrightarrow \exists a \in B x = a \cdot_{R} G)$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
19	1 3 18	dvdsr2	$⊢ G \in B \to (G \underset{˙}{∥} x \leftrightarrow \exists a \in B a \cdot_{R} G = x)$
20	19	adantl	$⊢ (R \in Ring \land G \in B) \to (G \underset{˙}{∥} x \leftrightarrow \exists a \in B a \cdot_{R} G = x)$
21	6 17 20	3bitr4d	$⊢ (R \in Ring \land G \in B) \to (x \in K (\{G\}) \leftrightarrow G \underset{˙}{∥} x)$
22	21	eqabdv	$⊢ (R \in Ring \land G \in B) \to K (\{G\}) = \{x \| G \underset{˙}{∥} x\}$

Metamath Proof Explorer

Theorem rspsn

Proof