Metamath Proof Explorer

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 𝑊 ) )