Theorem asclmul1

Description: Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	asclmul1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclmul1.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclmul1.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	asclmul1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	asclmul1.t	⊢ × = ( .r ‘ 𝑊 )
	asclmul1.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	asclmul1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑅 ) × 𝑋 ) = ( 𝑅 · 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		asclmul1.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclmul1.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclmul1.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
4		asclmul1.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
5		asclmul1.t	⊢ × = ( .r ‘ 𝑊 )
6		asclmul1.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
7		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
8	1 2 3 6 7	asclval	⊢ ( 𝑅 ∈ 𝐾 → ( 𝐴 ‘ 𝑅 ) = ( 𝑅 · ( 1r ‘ 𝑊 ) ) )
9	8	3ad2ant2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑅 ) = ( 𝑅 · ( 1r ‘ 𝑊 ) ) )
10	9	oveq1d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑅 ) × 𝑋 ) = ( ( 𝑅 · ( 1r ‘ 𝑊 ) ) × 𝑋 ) )
11		simp1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ AssAlg )
12		simp2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ∈ 𝐾 )
13		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
14	13	3ad2ant1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ Ring )
15	4 7	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝑉 )
16	14 15	syl	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 1r ‘ 𝑊 ) ∈ 𝑉 )
17		simp3	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
18	4 2 3 6 5	assaass	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑅 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑅 · ( 1r ‘ 𝑊 ) ) × 𝑋 ) = ( 𝑅 · ( ( 1r ‘ 𝑊 ) × 𝑋 ) ) )
19	11 12 16 17 18	syl13anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑅 · ( 1r ‘ 𝑊 ) ) × 𝑋 ) = ( 𝑅 · ( ( 1r ‘ 𝑊 ) × 𝑋 ) ) )
20	4 5 7	ringlidm	⊢ ( ( 𝑊 ∈ Ring ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝑊 ) × 𝑋 ) = 𝑋 )
21	14 17 20	syl2anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝑊 ) × 𝑋 ) = 𝑋 )
22	21	oveq2d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑅 · ( ( 1r ‘ 𝑊 ) × 𝑋 ) ) = ( 𝑅 · 𝑋 ) )
23	10 19 22	3eqtrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑅 ) × 𝑋 ) = ( 𝑅 · 𝑋 ) )