This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) = 𝐵 )