Metamath Proof Explorer

Theorem r1plmhm

Description: The univariate polynomial remainder function F is a module homomorphism. Its image ( F "s P ) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1plmhm.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1plmhm.2 ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1plmhm.4 ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1plmhm.5 ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1plmhm.6 ⊢ 𝐹 = ( 𝑓 ∈ 𝑈 ↦ ( 𝑓 𝐸 𝑀 ) )
r1plmhm.9 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
r1plmhm.10 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
Assertion r1plmhm ( 𝜑 → 𝐹 ∈ ( 𝑃 LMHom ( 𝐹 “s 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 r1plmhm.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1plmhm.2 ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1plmhm.4 ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
4 r1plmhm.5 ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
5 r1plmhm.6 ⊢ 𝐹 = ( 𝑓 ∈ 𝑈 ↦ ( 𝑓 𝐸 𝑀 ) )
6 r1plmhm.9 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 r1plmhm.10 ⊢ ( 𝜑 → 𝑀 ∈ 𝑁 )
8 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑅 ∈ Ring )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑓 ∈ 𝑈 )
10 7 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → 𝑀 ∈ 𝑁 )
11 3 1 2 4 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝑈 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑓 𝐸 𝑀 ) ∈ 𝑈 )
12 8 9 10 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑈 ) → ( 𝑓 𝐸 𝑀 ) ∈ 𝑈 )
13 12 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ 𝑈 )
14 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
15 anass ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ↔ ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) )
16 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑅 ∈ Ring )
17 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑎 ∈ 𝑈 )
18 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑀 ∈ 𝑁 )
19 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) )
20 oveq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 𝐸 𝑀 ) = ( 𝑎 𝐸 𝑀 ) )
21 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑎 𝐸 𝑀 ) ∈ V )
22 5 20 17 21 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝑎 𝐸 𝑀 ) )
23 oveq1 ⊢ ( 𝑓 = 𝑝 → ( 𝑓 𝐸 𝑀 ) = ( 𝑝 𝐸 𝑀 ) )
24 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑝 ∈ 𝑈 )
25 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑝 𝐸 𝑀 ) ∈ V )
26 5 23 24 25 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝑝 𝐸 𝑀 ) )
27 19 22 26 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑎 𝐸 𝑀 ) = ( 𝑝 𝐸 𝑀 ) )
28 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑏 ∈ 𝑈 )
29 1 2 4 3 16 17 18 27 14 24 28 r1padd1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) = ( ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
30 oveq1 ⊢ ( 𝑓 = ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
31 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
32 6 31 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
33 32 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
34 33 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑃 ∈ Grp )
35 2 14 34 17 28 grpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝑈 )
36 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) ∈ V )
37 5 30 35 36 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
38 oveq1 ⊢ ( 𝑓 = ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
39 2 14 34 24 28 grpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝑈 )
40 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) ∈ V )
41 5 38 39 40 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
42 29 37 41 3eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) ) )
43 32 ringabld ⊢ ( 𝜑 → 𝑃 ∈ Abel )
44 43 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑃 ∈ Abel )
45 2 14 ablcom ⊢ ( ( 𝑃 ∈ Abel ∧ 𝑝 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) )
46 44 24 28 45 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) )
47 46 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) ) )
48 42 47 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) ) )
49 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) )
50 oveq1 ⊢ ( 𝑓 = 𝑏 → ( 𝑓 𝐸 𝑀 ) = ( 𝑏 𝐸 𝑀 ) )
51 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑏 𝐸 𝑀 ) ∈ V )
52 5 50 28 51 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝑏 𝐸 𝑀 ) )
53 oveq1 ⊢ ( 𝑓 = 𝑞 → ( 𝑓 𝐸 𝑀 ) = ( 𝑞 𝐸 𝑀 ) )
54 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → 𝑞 ∈ 𝑈 )
55 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑞 𝐸 𝑀 ) ∈ V )
56 5 53 54 55 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝑞 𝐸 𝑀 ) )
57 49 52 56 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑏 𝐸 𝑀 ) = ( 𝑞 𝐸 𝑀 ) )
58 1 2 4 3 16 28 18 57 14 54 24 r1padd1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) = ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) )
59 oveq1 ⊢ ( 𝑓 = ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) )
60 2 14 34 28 24 grpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) ∈ 𝑈 )
61 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) ∈ V )
62 5 59 60 61 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) ) = ( ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) )
63 oveq1 ⊢ ( 𝑓 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) )
64 2 14 34 54 24 grpcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) ∈ 𝑈 )
65 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) ∈ V )
66 5 63 64 65 fvmptd3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) ) = ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) 𝐸 𝑀 ) )
67 58 62 66 3eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑃 ) 𝑝 ) ) = ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) ) )
68 2 14 ablcom ⊢ ( ( 𝑃 ∈ Abel ∧ 𝑞 ∈ 𝑈 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) = ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) )
69 44 54 24 68 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) = ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) )
70 69 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑝 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) )
71 48 67 70 3eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) )
72 71 expl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑞 ∈ 𝑈 ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
73 72 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑈 ) ∧ ( 𝑝 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
74 15 73 sylanbr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) ∧ ( 𝑝 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
75 74 3impa ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ∧ ( 𝑝 ∈ 𝑈 ∧ 𝑞 ∈ 𝑈 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑃 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑃 ) 𝑞 ) ) ) )
76 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
77 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
78 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
79 simpr2 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑈 )
80 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑎 𝐸 𝑀 ) ∈ V )
81 5 20 79 80 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝑎 𝐸 𝑀 ) )
82 simpr3 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑈 )
83 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑏 𝐸 𝑀 ) ∈ V )
84 5 50 82 83 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝑏 𝐸 𝑀 ) )
85 78 81 84 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑎 𝐸 𝑀 ) = ( 𝑏 𝐸 𝑀 ) )
86 85 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) ( 𝑎 𝐸 𝑀 ) ) = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) ( 𝑏 𝐸 𝑀 ) ) )
87 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
88 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑀 ∈ 𝑁 )
89 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
90 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
91 simpr1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
92 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
93 6 92 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
94 93 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
95 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
96 91 95 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑘 ∈ ( Base ‘ 𝑅 ) )
97 1 2 4 3 87 79 88 89 90 96 r1pvsca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) 𝐸 𝑀 ) = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) ( 𝑎 𝐸 𝑀 ) ) )
98 1 2 4 3 87 82 88 89 90 96 r1pvsca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) ( 𝑏 𝐸 𝑀 ) ) )
99 86 97 98 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) 𝐸 𝑀 ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
100 oveq1 ⊢ ( 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) 𝐸 𝑀 ) )
101 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
102 87 101 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑃 ∈ LMod )
103 2 76 89 77 102 91 79 lmodvscld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ∈ 𝑈 )
104 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) 𝐸 𝑀 ) ∈ V )
105 5 100 103 104 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) 𝐸 𝑀 ) )
106 oveq1 ⊢ ( 𝑓 = ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) → ( 𝑓 𝐸 𝑀 ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
107 2 76 89 77 102 91 82 lmodvscld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ 𝑈 )
108 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) ∈ V )
109 5 106 107 108 fvmptd3 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) 𝐸 𝑀 ) )
110 99 105 109 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ) )
111 110 an32s ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ) )
112 111 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) = ( 𝐹 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ) ) )
113 6 101 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
114 2 13 14 75 76 77 112 113 89 imaslmhm ⊢ ( 𝜑 → ( ( 𝐹 “s 𝑃 ) ∈ LMod ∧ 𝐹 ∈ ( 𝑃 LMHom ( 𝐹 “s 𝑃 ) ) ) )
115 114 simprd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 LMHom ( 𝐹 “s 𝑃 ) ) )