Metamath Proof Explorer

Theorem pmatcollpwscmatlem1

Description: Lemma 1 for pmatcollpwscmat . (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpwscmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpwscmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpwscmat.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpwscmat.m1 ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
pmatcollpwscmat.e1 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpwscmat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
pmatcollpwscmat.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
pmatcollpwscmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pmatcollpwscmat.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
pmatcollpwscmat.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
pmatcollpwscmat.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
pmatcollpwscmat.e2 ⊢ 𝐸 = ( Base ‘ 𝑃 )
pmatcollpwscmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
pmatcollpwscmat.1 ⊢ 1 = ( 1r ‘ 𝐶 )
pmatcollpwscmat.m2 ⊢ 𝑀 = ( 𝑄 ∗ 1 )
Assertion pmatcollpwscmatlem1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpwscmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pmatcollpwscmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pmatcollpwscmat.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pmatcollpwscmat.m1 ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5 pmatcollpwscmat.e1 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6 pmatcollpwscmat.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 pmatcollpwscmat.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8 pmatcollpwscmat.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
9 pmatcollpwscmat.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
10 pmatcollpwscmat.u ⊢ 𝑈 = ( algSc ‘ 𝑃 )
11 pmatcollpwscmat.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
12 pmatcollpwscmat.e2 ⊢ 𝐸 = ( Base ‘ 𝑃 )
13 pmatcollpwscmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
14 pmatcollpwscmat.1 ⊢ 1 = ( 1r ‘ 𝐶 )
15 pmatcollpwscmat.m2 ⊢ 𝑀 = ( 𝑄 ∗ 1 )
16 15 oveqi ⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑎 ( 𝑄 ∗ 1 ) 𝑏 )
17 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
18 17 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) )
19 simpr ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) → 𝑄 ∈ 𝐸 )
20 18 19 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ 𝑄 ∈ 𝐸 ) )
21 df-3an ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ 𝑄 ∈ 𝐸 ) )
22 20 21 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) )
23 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
24 2 12 23 14 4 scmatscmide ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑄 ∗ 1 ) 𝑏 ) = if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) )
25 22 24 sylan ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 ( 𝑄 ∗ 1 ) 𝑏 ) = if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) )
26 16 25 eqtrid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑀 𝑏 ) = if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) )
27 26 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( coe1 ‘ if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) ) )
28 27 fveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) = ( ( coe1 ‘ if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) ) ‘ 𝐿 ) )
29 fvif ⊢ ( coe1 ‘ if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) ) = if ( 𝑎 = 𝑏 , ( coe1 ‘ 𝑄 ) , ( coe1 ‘ ( 0g ‘ 𝑃 ) ) )
30 29 fveq1i ⊢ ( ( coe1 ‘ if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) ) ‘ 𝐿 ) = ( if ( 𝑎 = 𝑏 , ( coe1 ‘ 𝑄 ) , ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ) ‘ 𝐿 )
31 iffv ⊢ ( if ( 𝑎 = 𝑏 , ( coe1 ‘ 𝑄 ) , ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ) ‘ 𝐿 ) = if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) )
32 30 31 eqtri ⊢ ( ( coe1 ‘ if ( 𝑎 = 𝑏 , 𝑄 , ( 0g ‘ 𝑃 ) ) ) ‘ 𝐿 ) = if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) )
33 28 32 eqtrdi ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) = if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ) )
34 33 oveq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
35 ovif ⊢ ( if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
36 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
37 1 23 36 coe1z ⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ ( 0g ‘ 𝑃 ) ) = ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) )
38 37 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( coe1 ‘ ( 0g ‘ 𝑃 ) ) = ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) )
39 38 fveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) = ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝐿 ) )
40 fvexd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝑅 ) ∈ V )
41 simpl ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) → 𝐿 ∈ ℕ0 )
42 40 41 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 0g ‘ 𝑅 ) ∈ V ∧ 𝐿 ∈ ℕ0 ) )
43 fvconst2g ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ V ∧ 𝐿 ∈ ℕ0 ) → ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝐿 ) = ( 0g ‘ 𝑅 ) )
44 42 43 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ℕ0 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝐿 ) = ( 0g ‘ 𝑅 ) )
45 39 44 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) = ( 0g ‘ 𝑅 ) )
46 45 oveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
47 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
48 47 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → 𝑃 ∈ LMod )
49 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
50 49 12 mgpbas ⊢ 𝐸 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
51 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
52 49 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
53 17 52 syl ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
54 0nn0 ⊢ 0 ∈ ℕ0
55 54 a1i ⊢ ( 𝑅 ∈ Ring → 0 ∈ ℕ0 )
56 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
57 56 1 12 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ 𝐸 )
58 50 51 53 55 57 mulgnn0cld ⊢ ( 𝑅 ∈ Ring → ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝐸 )
59 58 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝐸 )
60 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
61 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
62 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
63 12 60 61 62 23 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝐸 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
64 48 59 63 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
65 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
66 65 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
67 66 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
68 67 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
69 68 eqeq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) )
70 69 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) ) )
71 64 70 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
72 46 71 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
73 72 ifeq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( 0g ‘ 𝑃 ) ) )
74 73 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( 0g ‘ 𝑃 ) ) )
75 35 74 eqtrid ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( if ( 𝑎 = 𝑏 , ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) , ( ( coe1 ‘ ( 0g ‘ 𝑃 ) ) ‘ 𝐿 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( 0g ‘ 𝑃 ) ) )
76 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) )
77 76 ancomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) )
78 eqid ⊢ ( coe1 ‘ 𝑄 ) = ( coe1 ‘ 𝑄 )
79 78 12 1 11 coe1fvalcl ⊢ ( ( 𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 )
80 77 79 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 )
81 65 eqcomd ⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
82 81 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
83 82 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
84 83 11 eqtr4di ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = 𝐾 )
85 84 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 ) )
86 85 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ 𝐾 ) )
87 80 86 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
88 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
89 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
90 10 60 88 61 89 asclval ⊢ ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) → ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) = ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
91 87 90 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) = ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
92 1 56 49 51 ply1idvr1 ⊢ ( 𝑅 ∈ Ring → ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
93 92 eqcomd ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑃 ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
94 93 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( 1r ‘ 𝑃 ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
95 94 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
96 91 95 eqtr2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) )
97 96 ifeq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) → if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( 0g ‘ 𝑃 ) ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )
98 97 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → if ( 𝑎 = 𝑏 , ( ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) , ( 0g ‘ 𝑃 ) ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )
99 34 75 98 3eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( ( coe1 ‘ ( 𝑎 𝑀 𝑏 ) ) ‘ 𝐿 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = if ( 𝑎 = 𝑏 , ( 𝑈 ‘ ( ( coe1 ‘ 𝑄 ) ‘ 𝐿 ) ) , ( 0g ‘ 𝑃 ) ) )