m2cpminvid2lem

Description: Lemma for m2cpminvid2 . (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminvid2lem.s	$⊢ S = N ConstPolyMat R$
	m2cpminvid2lem.p	$⊢ P = {Poly}_{1} (R)$
Assertion	m2cpminvid2lem	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to \forall n \in ℕ_{0} {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$

Proof

Step	Hyp	Ref	Expression
1		m2cpminvid2lem.s	$⊢ S = N ConstPolyMat R$
2		m2cpminvid2lem.p	$⊢ P = {Poly}_{1} (R)$
3		eqid	$⊢ N Mat P = N Mat P$
4		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
5	1 2 3 4	cpmatelimp	$⊢ (N \in Fin \land R \in Ring) \to (M \in S \to (M \in {Base}_{(N Mat P)} \land \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R}))$
6	5	3impia	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to (M \in {Base}_{(N Mat P)} \land \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R})$
7	6	simprd	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R}$
8	7	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to \forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R}$
9		fvoveq1	$⊢ i = x \to {coe}_{1} (i M j) = {coe}_{1} (x M j)$
10	9	fveq1d	$⊢ i = x \to {coe}_{1} (i M j) (k) = {coe}_{1} (x M j) (k)$
11	10	eqeq1d	$⊢ i = x \to ({coe}_{1} (i M j) (k) = 0_{R} \leftrightarrow {coe}_{1} (x M j) (k) = 0_{R})$
12	11	ralbidv	$⊢ i = x \to (\forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R} \leftrightarrow \forall k \in ℕ {coe}_{1} (x M j) (k) = 0_{R})$
13		oveq2	$⊢ j = y \to x M j = x M y$
14	13	fveq2d	$⊢ j = y \to {coe}_{1} (x M j) = {coe}_{1} (x M y)$
15	14	fveq1d	$⊢ j = y \to {coe}_{1} (x M j) (k) = {coe}_{1} (x M y) (k)$
16	15	eqeq1d	$⊢ j = y \to ({coe}_{1} (x M j) (k) = 0_{R} \leftrightarrow {coe}_{1} (x M y) (k) = 0_{R})$
17	16	ralbidv	$⊢ j = y \to (\forall k \in ℕ {coe}_{1} (x M j) (k) = 0_{R} \leftrightarrow \forall k \in ℕ {coe}_{1} (x M y) (k) = 0_{R})$
18	12 17	rspc2v	$⊢ (x \in N \land y \in N) \to (\forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R} \to \forall k \in ℕ {coe}_{1} (x M y) (k) = 0_{R})$
19	18	adantl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R} \to \forall k \in ℕ {coe}_{1} (x M y) (k) = 0_{R})$
20		fveqeq2	$⊢ k = n \to ({coe}_{1} (x M y) (k) = 0_{R} \leftrightarrow {coe}_{1} (x M y) (n) = 0_{R})$
21	20	cbvralvw	$⊢ \forall k \in ℕ {coe}_{1} (x M y) (k) = 0_{R} \leftrightarrow \forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R}$
22		simpl2	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to R \in Ring$
23		eqid	$⊢ {Base}_{P} = {Base}_{P}$
24		simprl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to x \in N$
25		simprr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to y \in N$
26	1 2 3 4	cpmatpmat	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to M \in {Base}_{(N Mat P)}$
27	26	adantr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to M \in {Base}_{(N Mat P)}$
28	3 23 4 24 25 27	matecld	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to x M y \in {Base}_{P}$
29		0nn0	$⊢ 0 \in ℕ_{0}$
30		eqid	$⊢ {coe}_{1} (x M y) = {coe}_{1} (x M y)$
31		eqid	$⊢ {Base}_{R} = {Base}_{R}$
32	30 23 2 31	coe1fvalcl	$⊢ (x M y \in {Base}_{P} \land 0 \in ℕ_{0}) \to {coe}_{1} (x M y) (0) \in {Base}_{R}$
33	28 29 32	sylancl	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to {coe}_{1} (x M y) (0) \in {Base}_{R}$
34	22 33	jca	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R})$
35	34	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R})$
36		eqid	$⊢ algSc (P) = algSc (P)$
37		eqid	$⊢ 0_{R} = 0_{R}$
38	2 36 31 37	coe1scl	$⊢ (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R}) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) = (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R}))$
39	35 38	syl	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) = (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R}))$
40	39	fveq1d	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R})) (n)$
41		eqidd	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R})) = (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R}))$
42		eqeq1	$⊢ l = n \to (l = 0 \leftrightarrow n = 0)$
43	42	ifbid	$⊢ l = n \to if (l = 0, {coe}_{1} (x M y) (0), 0_{R}) = if (n = 0, {coe}_{1} (x M y) (0), 0_{R})$
44	43	adantl	$⊢ ((((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \land l = n) \to if (l = 0, {coe}_{1} (x M y) (0), 0_{R}) = if (n = 0, {coe}_{1} (x M y) (0), 0_{R})$
45		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
46	45	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to n \in ℕ_{0}$
47		fvex	$⊢ {coe}_{1} (x M y) (0) \in V$
48		fvex	$⊢ 0_{R} \in V$
49	47 48	ifex	$⊢ if (n = 0, {coe}_{1} (x M y) (0), 0_{R}) \in V$
50	49	a1i	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to if (n = 0, {coe}_{1} (x M y) (0), 0_{R}) \in V$
51	41 44 46 50	fvmptd	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to (l \in ℕ_{0} ⟼ if (l = 0, {coe}_{1} (x M y) (0), 0_{R})) (n) = if (n = 0, {coe}_{1} (x M y) (0), 0_{R})$
52		nnne0	$⊢ n \in ℕ \to n \neq 0$
53	52	neneqd	$⊢ n \in ℕ \to \neg n = 0$
54	53	adantl	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to \neg n = 0$
55	54	iffalsed	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to if (n = 0, {coe}_{1} (x M y) (0), 0_{R}) = 0_{R}$
56	40 51 55	3eqtrd	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = 0_{R}$
57		eqcom	$⊢ {coe}_{1} (x M y) (n) = 0_{R} \leftrightarrow 0_{R} = {coe}_{1} (x M y) (n)$
58	57	biimpi	$⊢ {coe}_{1} (x M y) (n) = 0_{R} \to 0_{R} = {coe}_{1} (x M y) (n)$
59	56 58	sylan9eq	$⊢ ((((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \land {coe}_{1} (x M y) (n) = 0_{R}) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$
60	59	ex	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land n \in ℕ) \to ({coe}_{1} (x M y) (n) = 0_{R} \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n))$
61	60	ralimdva	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R} \to \forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n))$
62	61	imp	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land \forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R}) \to \forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$
63	34	adantr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land \forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R}) \to (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R})$
64	2 36 31	ply1sclid	$⊢ (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R}) \to {coe}_{1} (x M y) (0) = {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0)$
65	64	eqcomd	$⊢ (R \in Ring \land {coe}_{1} (x M y) (0) \in {Base}_{R}) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)$
66	63 65	syl	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land \forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R}) \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)$
67	62 66	jca	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \land \forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R}) \to (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0))$
68	67	ex	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall n \in ℕ {coe}_{1} (x M y) (n) = 0_{R} \to (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)))$
69	21 68	syl5bi	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall k \in ℕ {coe}_{1} (x M y) (k) = 0_{R} \to (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)))$
70	19 69	syld	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall i \in N \forall j \in N \forall k \in ℕ {coe}_{1} (i M j) (k) = 0_{R} \to (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)))$
71	8 70	mpd	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0))$
72		c0ex	$⊢ 0 \in V$
73		fveq2	$⊢ n = 0 \to {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0)$
74		fveq2	$⊢ n = 0 \to {coe}_{1} (x M y) (n) = {coe}_{1} (x M y) (0)$
75	73 74	eqeq12d	$⊢ n = 0 \to ({coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \leftrightarrow {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0))$
76	75	ralunsn	$⊢ 0 \in V \to (\forall n \in (ℕ \cup \{0\}) {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \leftrightarrow (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)))$
77	72 76	mp1i	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to (\forall n \in (ℕ \cup \{0\}) {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \leftrightarrow (\forall n \in ℕ {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \land {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (0) = {coe}_{1} (x M y) (0)))$
78	71 77	mpbird	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to \forall n \in (ℕ \cup \{0\}) {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$
79		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
80	79	raleqi	$⊢ \forall n \in ℕ_{0} {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n) \leftrightarrow \forall n \in (ℕ \cup \{0\}) {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$
81	78 80	sylibr	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (x \in N \land y \in N)) \to \forall n \in ℕ_{0} {coe}_{1} (algSc (P) ({coe}_{1} (x M y) (0))) (n) = {coe}_{1} (x M y) (n)$

Metamath Proof Explorer

Theorem m2cpminvid2lem

Proof