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

Metamath Proof Explorer

Theorem rnascl

Description: The set of lifted scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses rnascl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
rnascl.o ⊢ 1 = ( 1r ‘ 𝑊 )
rnascl.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion rnascl ( 𝑊 ∈ AssAlg → ran 𝐴 = ( 𝑁 ‘ { 1 } ) )

Proof

Step Hyp Ref Expression
1 rnascl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 rnascl.o ⊢ 1 = ( 1r ‘ 𝑊 )
3 rnascl.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7 1 4 5 6 2 asclfval ⊢ 𝐴 = ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↦ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) )
8 7 rnmpt ⊢ ran 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) }
9 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
10 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
11 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 11 2 ringidcl ⊢ ( 𝑊 ∈ Ring → 1 ∈ ( Base ‘ 𝑊 ) )
13 10 12 syl ⊢ ( 𝑊 ∈ AssAlg → 1 ∈ ( Base ‘ 𝑊 ) )
14 4 5 11 6 3 lspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
15 9 13 14 syl2anc ⊢ ( 𝑊 ∈ AssAlg → ( 𝑁 ‘ { 1 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 1 ) } )
16 8 15 eqtr4id ⊢ ( 𝑊 ∈ AssAlg → ran 𝐴 = ( 𝑁 ‘ { 1 } ) )