pmatcollpwscmatlem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pmatcollpwscmatlem1		Structured version Visualization version GIF version

Theorem pmatcollpwscmatlem1 22513

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

**Hypotheses**
Ref	Expression
pmatcollpwscmat.p	⊢ 𝑃 = (Poly₁‘𝑅)
pmatcollpwscmat.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
pmatcollpwscmat.b	⊢ 𝐵 = (Base‘𝐶)
pmatcollpwscmat.m1	⊢ ∗ = ( ·_𝑠 ‘𝐶)
pmatcollpwscmat.e1	⊢ ↑ = (._g‘(mulGrp‘𝑃))
pmatcollpwscmat.x	⊢ 𝑋 = (var₁‘𝑅)
pmatcollpwscmat.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
pmatcollpwscmat.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
pmatcollpwscmat.d	⊢ 𝐷 = (Base‘𝐴)
pmatcollpwscmat.u	⊢ 𝑈 = (algSc‘𝑃)
pmatcollpwscmat.k	⊢ 𝐾 = (Base‘𝑅)
pmatcollpwscmat.e2	⊢ 𝐸 = (Base‘𝑃)
pmatcollpwscmat.s	⊢ 𝑆 = (algSc‘𝑃)
pmatcollpwscmat.1	⊢ 1 = (1_r‘𝐶)
pmatcollpwscmat.m2	⊢ 𝑀 = (𝑄 ∗ 1 )

**Assertion**
Ref	Expression
pmatcollpwscmatlem1	⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe₁‘(𝑎𝑀𝑏))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe₁‘𝑄)‘𝐿)), (0_g‘𝑃)))

**Proof of Theorem pmatcollpwscmatlem1**
Step	Hyp	Ref	Expression
1		pmatcollpwscmat.m2	. . . . . . . 8 ⊢ 𝑀 = (𝑄 ∗ 1 )
2	1	oveqi 7426	. . . . . . 7 ⊢ (𝑎𝑀𝑏) = (𝑎(𝑄 ∗ 1 )𝑏)
3		pmatcollpwscmat.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly₁‘𝑅)
4	3	ply1ring 21992	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
5	4	anim2i 615	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring))
6		simpr 483	. . . . . . . . . 10 ⊢ ((𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸) → 𝑄 ∈ 𝐸)
7	5, 6	anim12i 611	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ 𝑄 ∈ 𝐸))
8		df-3an 1087	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸) ↔ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ 𝑄 ∈ 𝐸))
9	7, 8	sylibr 233	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸))
10		pmatcollpwscmat.c	. . . . . . . . 9 ⊢ 𝐶 = (𝑁 Mat 𝑃)
11		pmatcollpwscmat.e2	. . . . . . . . 9 ⊢ 𝐸 = (Base‘𝑃)
12		eqid 2730	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
13		pmatcollpwscmat.1	. . . . . . . . 9 ⊢ 1 = (1_r‘𝐶)
14		pmatcollpwscmat.m1	. . . . . . . . 9 ⊢ ∗ = ( ·_𝑠 ‘𝐶)
15	10, 11, 12, 13, 14	scmatscmide 22231	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))
16	9, 15	sylan 578	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))
17	2, 16	eqtrid 2782	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎𝑀𝑏) = if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))
18	17	fveq2d 6896	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (coe₁‘(𝑎𝑀𝑏)) = (coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃))))
19	18	fveq1d 6894	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ((coe₁‘(𝑎𝑀𝑏))‘𝐿) = ((coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))‘𝐿))
20		fvif 6908	. . . . . 6 ⊢ (coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃))) = if(𝑎 = 𝑏, (coe₁‘𝑄), (coe₁‘(0_g‘𝑃)))
21	20	fveq1i 6893	. . . . 5 ⊢ ((coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))‘𝐿) = (if(𝑎 = 𝑏, (coe₁‘𝑄), (coe₁‘(0_g‘𝑃)))‘𝐿)
22		iffv 6909	. . . . 5 ⊢ (if(𝑎 = 𝑏, (coe₁‘𝑄), (coe₁‘(0_g‘𝑃)))‘𝐿) = if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))
23	21, 22	eqtri 2758	. . . 4 ⊢ ((coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))‘𝐿) = if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))
24	19, 23	eqtrdi 2786	. . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ((coe₁‘(𝑎𝑀𝑏))‘𝐿) = if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿)))
25	24	oveq1d 7428	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe₁‘(𝑎𝑀𝑏))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
26		ovif 7510	. . 3 ⊢ (if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
27		eqid 2730	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
28	3, 12, 27	coe1z 22007	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (coe₁‘(0_g‘𝑃)) = (ℕ₀ × {(0_g‘𝑅)}))
29	28	ad2antlr 723	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (coe₁‘(0_g‘𝑃)) = (ℕ₀ × {(0_g‘𝑅)}))
30	29	fveq1d 6894	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘(0_g‘𝑃))‘𝐿) = ((ℕ₀ × {(0_g‘𝑅)})‘𝐿))
31		fvexd 6907	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝑅) ∈ V)
32		simpl 481	. . . . . . . . . 10 ⊢ ((𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸) → 𝐿 ∈ ℕ₀)
33	31, 32	anim12i 611	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘𝑅) ∈ V ∧ 𝐿 ∈ ℕ₀))
34		fvconst2g 7206	. . . . . . . . 9 ⊢ (((0_g‘𝑅) ∈ V ∧ 𝐿 ∈ ℕ₀) → ((ℕ₀ × {(0_g‘𝑅)})‘𝐿) = (0_g‘𝑅))
35	33, 34	syl 17	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((ℕ₀ × {(0_g‘𝑅)})‘𝐿) = (0_g‘𝑅))
36	30, 35	eqtrd 2770	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘(0_g‘𝑃))‘𝐿) = (0_g‘𝑅))
37	36	oveq1d 7428	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
38	3	ply1lmod 21996	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
39	38	ad2antlr 723	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → 𝑃 ∈ LMod)
40		eqid 2730	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
41	40, 11	mgpbas 20036	. . . . . . . . . 10 ⊢ 𝐸 = (Base‘(mulGrp‘𝑃))
42		eqid 2730	. . . . . . . . . 10 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
43	40	ringmgp 20135	. . . . . . . . . . 11 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
44	4, 43	syl 17	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
45		0nn0 12493	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
46	45	a1i 11	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 0 ∈ ℕ₀)
47		eqid 2730	. . . . . . . . . . 11 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
48	47, 3, 11	vr1cl 21962	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ 𝐸)
49	41, 42, 44, 46, 48	mulgnn0cld 19013	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸)
50	49	ad2antlr 723	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸)
51		eqid 2730	. . . . . . . . 9 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
52		eqid 2730	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
53		eqid 2730	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
54	11, 51, 52, 53, 12	lmod0vs 20651	. . . . . . . 8 ⊢ ((𝑃 ∈ LMod ∧ (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
55	39, 50, 54	syl2anc 582	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
56	3	ply1sca 21997	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
57	56	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃))
58	57	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
59	58	oveq1d 7428	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
60	59	eqeq1d 2732	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃) ↔ ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃)))
61	60	adantr 479	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃) ↔ ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃)))
62	55, 61	mpbird 256	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
63	37, 62	eqtrd 2770	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
64	63	ifeq2d 4549	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)))
65	64	adantr 479	. . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)))
66	26, 65	eqtrid 2782	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)))
67		simpr 483	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸))
68	67	ancomd 460	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ₀))
69		eqid 2730	. . . . . . . . 9 ⊢ (coe₁‘𝑄) = (coe₁‘𝑄)
70		pmatcollpwscmat.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑅)
71	69, 11, 3, 70	coe1fvalcl 21957	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ₀) → ((coe₁‘𝑄)‘𝐿) ∈ 𝐾)
72	68, 71	syl 17	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘𝑄)‘𝐿) ∈ 𝐾)
73	56	eqcomd 2736	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
74	73	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Scalar‘𝑃) = 𝑅)
75	74	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
76	75, 70	eqtr4di 2788	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(Scalar‘𝑃)) = 𝐾)
77	76	eleq2d 2817	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑄)‘𝐿) ∈ 𝐾))
78	77	adantr 479	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑄)‘𝐿) ∈ 𝐾))
79	72, 78	mpbird 256	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)))
80		pmatcollpwscmat.u	. . . . . . 7 ⊢ 𝑈 = (algSc‘𝑃)
81		eqid 2730	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
82		eqid 2730	. . . . . . 7 ⊢ (1_r‘𝑃) = (1_r‘𝑃)
83	80, 51, 81, 52, 82	asclval 21655	. . . . . 6 ⊢ (((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) → (𝑈‘((coe₁‘𝑄)‘𝐿)) = (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(1_r‘𝑃)))
84	79, 83	syl 17	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝑈‘((coe₁‘𝑄)‘𝐿)) = (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(1_r‘𝑃)))
85	3, 47, 40, 42	ply1idvr1 22039	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (1_r‘𝑃))
86	85	eqcomd 2736	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (1_r‘𝑃) = (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
87	86	ad2antlr 723	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (1_r‘𝑃) = (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
88	87	oveq2d 7429	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(1_r‘𝑃)) = (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
89	84, 88	eqtr2d 2771	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (𝑈‘((coe₁‘𝑄)‘𝐿)))
90	89	ifeq1d 4548	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)) = if(𝑎 = 𝑏, (𝑈‘((coe₁‘𝑄)‘𝐿)), (0_g‘𝑃)))
91	90	adantr 479	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)) = if(𝑎 = 𝑏, (𝑈‘((coe₁‘𝑄)‘𝐿)), (0_g‘𝑃)))
92	25, 66, 91	3eqtrd 2774	1 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe₁‘(𝑎𝑀𝑏))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe₁‘𝑄)‘𝐿)), (0_g‘𝑃)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 Vcvv 3472 ifcif 4529 {csn 4629 × cxp 5675 ‘cfv 6544 (class class class)co 7413 Fincfn 8943 0cc0 11114 ℕ₀cn0 12478 Basecbs 17150 Scalarcsca 17206 ·_𝑠 cvsca 17207 0_gc0g 17391 Mndcmnd 18661 ._gcmg 18988 mulGrpcmgp 20030 1_rcur 20077 Ringcrg 20129 LModclmod 20616 algSccascl 21628 var₁cv1 21921 Poly₁cpl1 21922 coe₁cco1 21923 Mat cmat 22129 matToPolyMat cmat2pmat 22428

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-ot 4638 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7674 df-ofr 7675 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8151 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-1o 8470 df-er 8707 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9366 df-sup 9441 df-oi 9509 df-card 9938 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11452 df-neg 11453 df-nn 12219 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-7 12286 df-8 12287 df-9 12288 df-n0 12479 df-z 12565 df-dec 12684 df-uz 12829 df-fz 13491 df-fzo 13634 df-seq 13973 df-hash 14297 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-hom 17227 df-cco 17228 df-0g 17393 df-gsum 17394 df-prds 17399 df-pws 17401 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18707 df-submnd 18708 df-grp 18860 df-minusg 18861 df-sbg 18862 df-mulg 18989 df-subg 19041 df-ghm 19130 df-cntz 19224 df-cmn 19693 df-abl 19694 df-mgp 20031 df-rng 20049 df-ur 20078 df-ring 20131 df-subrng 20436 df-subrg 20461 df-lmod 20618 df-lss 20689 df-sra 20932 df-rgmod 20933 df-dsmm 21508 df-frlm 21523 df-ascl 21631 df-psr 21683 df-mvr 21684 df-mpl 21685 df-opsr 21687 df-psr1 21925 df-vr1 21926 df-ply1 21927 df-coe1 21928 df-mamu 22108 df-mat 22130

This theorem is referenced by: pmatcollpwscmatlem2 22514

W3C validator