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 22291

Description: Lemma 1 for pmatcollpwscmat 22293. (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 7422	. . . . . . 7 ⊢ (𝑎𝑀𝑏) = (𝑎(𝑄 ∗ 1 )𝑏)
3		pmatcollpwscmat.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly₁‘𝑅)
4	3	ply1ring 21770	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
5	4	anim2i 618	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑁 ∈ Fin ∧ 𝑃 ∈ Ring))
6		simpr 486	. . . . . . . . . 10 ⊢ ((𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸) → 𝑄 ∈ 𝐸)
7	5, 6	anim12i 614	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) ∧ 𝑄 ∈ 𝐸))
8		df-3an 1090	. . . . . . . . 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 2733	. . . . . . . . 9 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
13		pmatcollpwscmat.1	. . . . . . . . 9 ⊢ 1 = (1_r‘𝐶)
14		pmatcollpwscmat.m1	. . . . . . . . 9 ⊢ ∗ = ( ·_𝑠 ‘𝐶)
15	10, 11, 12, 13, 14	scmatscmide 22009	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ∧ 𝑄 ∈ 𝐸) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))
16	9, 15	sylan 581	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (𝑎(𝑄 ∗ 1 )𝑏) = if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))
17	2, 16	eqtrid 2785	. . . . . 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 2761	. . . 4 ⊢ ((coe₁‘if(𝑎 = 𝑏, 𝑄, (0_g‘𝑃)))‘𝐿) = if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))
24	19, 23	eqtrdi 2789	. . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → ((coe₁‘(𝑎𝑀𝑏))‘𝐿) = if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿)))
25	24	oveq1d 7424	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe₁‘(𝑎𝑀𝑏))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
26		ovif 7506	. . 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 2733	. . . . . . . . . . 11 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
28	3, 12, 27	coe1z 21785	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (coe₁‘(0_g‘𝑃)) = (ℕ₀ × {(0_g‘𝑅)}))
29	28	ad2antlr 726	. . . . . . . . 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 484	. . . . . . . . . 10 ⊢ ((𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸) → 𝐿 ∈ ℕ₀)
33	31, 32	anim12i 614	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘𝑅) ∈ V ∧ 𝐿 ∈ ℕ₀))
34		fvconst2g 7203	. . . . . . . . 9 ⊢ (((0_g‘𝑅) ∈ V ∧ 𝐿 ∈ ℕ₀) → ((ℕ₀ × {(0_g‘𝑅)})‘𝐿) = (0_g‘𝑅))
35	33, 34	syl 17	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((ℕ₀ × {(0_g‘𝑅)})‘𝐿) = (0_g‘𝑅))
36	30, 35	eqtrd 2773	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘(0_g‘𝑃))‘𝐿) = (0_g‘𝑅))
37	36	oveq1d 7424	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘(0_g‘𝑃))‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
38	3	ply1lmod 21774	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
39	38	ad2antlr 726	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → 𝑃 ∈ LMod)
40		eqid 2733	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
41	40, 11	mgpbas 19993	. . . . . . . . . 10 ⊢ 𝐸 = (Base‘(mulGrp‘𝑃))
42		eqid 2733	. . . . . . . . . 10 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
43	40	ringmgp 20062	. . . . . . . . . . 11 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
44	4, 43	syl 17	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
45		0nn0 12487	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ₀
46	45	a1i 11	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 0 ∈ ℕ₀)
47		eqid 2733	. . . . . . . . . . 11 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
48	47, 3, 11	vr1cl 21741	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ 𝐸)
49	41, 42, 44, 46, 48	mulgnn0cld 18975	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸)
50	49	ad2antlr 726	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸)
51		eqid 2733	. . . . . . . . 9 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
52		eqid 2733	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
53		eqid 2733	. . . . . . . . 9 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
54	11, 51, 52, 53, 12	lmod0vs 20505	. . . . . . . 8 ⊢ ((𝑃 ∈ LMod ∧ (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝐸) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
55	39, 50, 54	syl2anc 585	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
56	3	ply1sca 21775	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
57	56	adantl 483	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃))
58	57	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
59	58	oveq1d 7424	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
60	59	eqeq1d 2735	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃) ↔ ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃)))
61	60	adantr 482	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃) ↔ ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃)))
62	55, 61	mpbird 257	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
63	37, 62	eqtrd 2773	. . . . 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 482	. . 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 2785	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (if(𝑎 = 𝑏, ((coe₁‘𝑄)‘𝐿), ((coe₁‘(0_g‘𝑃))‘𝐿))( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)))
67		simpr 486	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸))
68	67	ancomd 463	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ₀))
69		eqid 2733	. . . . . . . . 9 ⊢ (coe₁‘𝑄) = (coe₁‘𝑄)
70		pmatcollpwscmat.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝑅)
71	69, 11, 3, 70	coe1fvalcl 21736	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝐸 ∧ 𝐿 ∈ ℕ₀) → ((coe₁‘𝑄)‘𝐿) ∈ 𝐾)
72	68, 71	syl 17	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘𝑄)‘𝐿) ∈ 𝐾)
73	56	eqcomd 2739	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
74	73	adantl 483	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Scalar‘𝑃) = 𝑅)
75	74	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅))
76	75, 70	eqtr4di 2791	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘(Scalar‘𝑃)) = 𝐾)
77	76	eleq2d 2820	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑄)‘𝐿) ∈ 𝐾))
78	77	adantr 482	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑄)‘𝐿) ∈ 𝐾))
79	72, 78	mpbird 257	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → ((coe₁‘𝑄)‘𝐿) ∈ (Base‘(Scalar‘𝑃)))
80		pmatcollpwscmat.u	. . . . . . 7 ⊢ 𝑈 = (algSc‘𝑃)
81		eqid 2733	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
82		eqid 2733	. . . . . . 7 ⊢ (1_r‘𝑃) = (1_r‘𝑃)
83	80, 51, 81, 52, 82	asclval 21434	. . . . . 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 21817	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (1_r‘𝑃))
86	85	eqcomd 2739	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (1_r‘𝑃) = (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
87	86	ad2antlr 726	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (1_r‘𝑃) = (0(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
88	87	oveq2d 7425	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) → (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(1_r‘𝑃)) = (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
89	84, 88	eqtr2d 2774	. . . 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 482	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ₀ ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → if(𝑎 = 𝑏, (((coe₁‘𝑄)‘𝐿)( ·_𝑠 ‘𝑃)(0(._g‘(mulGrp‘𝑃))(var₁‘𝑅))), (0_g‘𝑃)) = if(𝑎 = 𝑏, (𝑈‘((coe₁‘𝑄)‘𝐿)), (0_g‘𝑃)))
92	25, 66, 91	3eqtrd 2777	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 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 Vcvv 3475 ifcif 4529 {csn 4629 × cxp 5675 ‘cfv 6544 (class class class)co 7409 Fincfn 8939 0cc0 11110 ℕ₀cn0 12472 Basecbs 17144 Scalarcsca 17200 ·_𝑠 cvsca 17201 0_gc0g 17385 Mndcmnd 18625 ._gcmg 18950 mulGrpcmgp 19987 1_rcur 20004 Ringcrg 20056 LModclmod 20471 algSccascl 21407 var₁cv1 21700 Poly₁cpl1 21701 coe₁cco1 21702 Mat cmat 21907 matToPolyMat cmat2pmat 22206

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 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 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7670 df-ofr 7671 df-om 7856 df-1st 7975 df-2nd 7976 df-supp 8147 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9362 df-sup 9437 df-oi 9505 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-fz 13485 df-fzo 13628 df-seq 13967 df-hash 14291 df-struct 17080 df-sets 17097 df-slot 17115 df-ndx 17127 df-base 17145 df-ress 17174 df-plusg 17210 df-mulr 17211 df-sca 17213 df-vsca 17214 df-ip 17215 df-tset 17216 df-ple 17217 df-ds 17219 df-hom 17221 df-cco 17222 df-0g 17387 df-gsum 17388 df-prds 17393 df-pws 17395 df-mre 17530 df-mrc 17531 df-acs 17533 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-mhm 18671 df-submnd 18672 df-grp 18822 df-minusg 18823 df-sbg 18824 df-mulg 18951 df-subg 19003 df-ghm 19090 df-cntz 19181 df-cmn 19650 df-abl 19651 df-mgp 19988 df-ur 20005 df-ring 20058 df-subrg 20317 df-lmod 20473 df-lss 20543 df-sra 20785 df-rgmod 20786 df-dsmm 21287 df-frlm 21302 df-ascl 21410 df-psr 21462 df-mvr 21463 df-mpl 21464 df-opsr 21466 df-psr1 21704 df-vr1 21705 df-ply1 21706 df-coe1 21707 df-mamu 21886 df-mat 21908

This theorem is referenced by: pmatcollpwscmatlem2 22292

W3C validator