Theorem rsp1

Description: The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	rspcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rsp1.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	rsp1	⊢ ( 𝑅 ∈ Ring → ( 𝐾 ‘ { 1 } ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
2		rspcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		rsp1.o	⊢ 1 = ( 1r ‘ 𝑅 )
4	2 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
5	4	snssd	⊢ ( 𝑅 ∈ Ring → { 1 } ⊆ 𝐵 )
6	1 2	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ { 1 } ⊆ 𝐵 ) → { 1 } ⊆ ( 𝐾 ‘ { 1 } ) )
7	5 6	mpdan	⊢ ( 𝑅 ∈ Ring → { 1 } ⊆ ( 𝐾 ‘ { 1 } ) )
8	3	fvexi	⊢ 1 ∈ V
9	8	snss	⊢ ( 1 ∈ ( 𝐾 ‘ { 1 } ) ↔ { 1 } ⊆ ( 𝐾 ‘ { 1 } ) )
10	7 9	sylibr	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( 𝐾 ‘ { 1 } ) )
11		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
12	1 2 11	rspcl	⊢ ( ( 𝑅 ∈ Ring ∧ { 1 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 1 } ) ∈ ( LIdeal ‘ 𝑅 ) )
13	5 12	mpdan	⊢ ( 𝑅 ∈ Ring → ( 𝐾 ‘ { 1 } ) ∈ ( LIdeal ‘ 𝑅 ) )
14	11 2 3	lidl1el	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐾 ‘ { 1 } ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( 1 ∈ ( 𝐾 ‘ { 1 } ) ↔ ( 𝐾 ‘ { 1 } ) = 𝐵 ) )
15	13 14	mpdan	⊢ ( 𝑅 ∈ Ring → ( 1 ∈ ( 𝐾 ‘ { 1 } ) ↔ ( 𝐾 ‘ { 1 } ) = 𝐵 ) )
16	10 15	mpbid	⊢ ( 𝑅 ∈ Ring → ( 𝐾 ‘ { 1 } ) = 𝐵 )