Theorem ressascl

Description: The injection 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 ‘ 𝑋 ) )