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

Metamath Proof Explorer

Theorem ressascl

Description: The lifting of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses ressascl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ressascl.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑆 )
Assertion ressascl ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 = ( algSc ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ressascl.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 ressascl.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑆 )
3 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4 2 3 resssca ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
5 4 fveq2d ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) ) )
6 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
7 2 6 ressvsca ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
8 eqidd ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑥 = 𝑥 )
9 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
10 2 9 subrg1 ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑋 ) )
11 7 8 10 oveq123d ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑋 ) ( 1r ‘ 𝑋 ) ) )
12 5 11 mpteq12dv ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) ( 1r ‘ 𝑋 ) ) ) )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
14 1 3 13 6 9 asclfval ⊢ 𝐴 = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
15 eqid ⊢ ( algSc ‘ 𝑋 ) = ( algSc ‘ 𝑋 )
16 eqid ⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
17 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) )
18 eqid ⊢ ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑋 )
19 eqid ⊢ ( 1r ‘ 𝑋 ) = ( 1r ‘ 𝑋 )
20 15 16 17 18 19 asclfval ⊢ ( algSc ‘ 𝑋 ) = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ↦ ( 𝑥 ( ·𝑠 ‘ 𝑋 ) ( 1r ‘ 𝑋 ) ) )
21 12 14 20 3eqtr4g ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝐴 = ( algSc ‘ 𝑋 ) )