Theorem asclghm

Description: The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	asclf.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclf.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclf.r	⊢ ( 𝜑 → 𝑊 ∈ Ring )
	asclf.l	⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion	asclghm	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 GrpHom 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		asclf.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclf.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclf.r	⊢ ( 𝜑 → 𝑊 ∈ Ring )
4		asclf.l	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7		eqid	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
8		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
9	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
10	4 9	syl	⊢ ( 𝜑 → 𝐹 ∈ Ring )
11		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
12	10 11	syl	⊢ ( 𝜑 → 𝐹 ∈ Grp )
13		ringgrp	⊢ ( 𝑊 ∈ Ring → 𝑊 ∈ Grp )
14	3 13	syl	⊢ ( 𝜑 → 𝑊 ∈ Grp )
15	1 2 3 4 5 6	asclf	⊢ ( 𝜑 → 𝐴 : ( Base ‘ 𝐹 ) ⟶ ( Base ‘ 𝑊 ) )
16	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → 𝑊 ∈ LMod )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
18		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐹 ) )
19		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
20	6 19	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
21	3 20	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
23		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
24	6 8 2 23 5 7	lmodvsdir	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( +g ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
25	16 17 18 22 24	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( +g ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
26	5 7	grpcl	⊢ ( ( 𝐹 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
27	26	3expb	⊢ ( ( 𝐹 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
28	12 27	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ∈ ( Base ‘ 𝐹 ) )
29	1 2 5 23 19	asclval	⊢ ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
30	28 29	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝐴 ‘ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
31	1 2 5 23 19	asclval	⊢ ( 𝑥 ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
32	1 2 5 23 19	asclval	⊢ ( 𝑦 ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ 𝑦 ) = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
33	31 32	oveqan12d	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( +g ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
34	33	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ( +g ‘ 𝑊 ) ( 𝑦 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ) )
35	25 30 34	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝐴 ‘ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( +g ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) )
36	5 6 7 8 12 14 15 35	isghmd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 GrpHom 𝑊 ) )