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 ‘ 𝑃 ) ) )