pm2mpf1

Description: The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019) (Revised by AV, 6-Dec-2019)

	Ref	Expression
Hypotheses	pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
	pm2mpval.c	$⊢ C = N Mat P$
	pm2mpval.b	$⊢ B = {Base}_{C}$
	pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
	pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
	pm2mpval.x	$⊢ X = {var}_{1} (A)$
	pm2mpval.a	$⊢ A = N Mat R$
	pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpval.t	$⊢ T = N pMatToMatPoly R$
	pm2mpcl.l	$⊢ L = {Base}_{Q}$
Assertion	pm2mpf1	$⊢ (N \in Fin \land R \in Ring) \to T : B \underset{1-1}{⟶} L$

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpval.c	$⊢ C = N Mat P$
3		pm2mpval.b	$⊢ B = {Base}_{C}$
4		pm2mpval.m	$⊢ \underset{˙}{*} = \cdot_{Q}$
5		pm2mpval.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{Q}}$
6		pm2mpval.x	$⊢ X = {var}_{1} (A)$
7		pm2mpval.a	$⊢ A = N Mat R$
8		pm2mpval.q	$⊢ Q = {Poly}_{1} (A)$
9		pm2mpval.t	$⊢ T = N pMatToMatPoly R$
10		pm2mpcl.l	$⊢ L = {Base}_{Q}$
11	1 2 3 4 5 6 7 8 9 10	pm2mpf	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ L$
12	7	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
13	12	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to A \in Ring$
14	1 2 3 4 5 6 7 8 9 10	pm2mpcl	$⊢ (N \in Fin \land R \in Ring \land u \in B) \to T (u) \in L$
15	14	3expa	$⊢ ((N \in Fin \land R \in Ring) \land u \in B) \to T (u) \in L$
16	15	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to T (u) \in L$
17	1 2 3 4 5 6 7 8 9 10	pm2mpcl	$⊢ (N \in Fin \land R \in Ring \land w \in B) \to T (w) \in L$
18	17	3expia	$⊢ (N \in Fin \land R \in Ring) \to (w \in B \to T (w) \in L)$
19	18	adantld	$⊢ (N \in Fin \land R \in Ring) \to ((u \in B \land w \in B) \to T (w) \in L)$
20	19	imp	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to T (w) \in L$
21		eqid	$⊢ {coe}_{1} (T (u)) = {coe}_{1} (T (u))$
22		eqid	$⊢ {coe}_{1} (T (w)) = {coe}_{1} (T (w))$
23	8 10 21 22	ply1coe1eq	$⊢ (A \in Ring \land T (u) \in L \land T (w) \in L) \to (\forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n) \leftrightarrow T (u) = T (w))$
24	23	bicomd	$⊢ (A \in Ring \land T (u) \in L \land T (w) \in L) \to (T (u) = T (w) \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n))$
25	13 16 20 24	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (T (u) = T (w) \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n))$
26		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to N \in Fin$
27		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to R \in Ring$
28		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to u \in B$
29	1 2 3 4 5 6 7 8 9	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land u \in B) \to T (u) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
30	26 27 28 29	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to T (u) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
31	30	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to T (u) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
32	31	fveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (T (u)) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
33	32	fveq1d	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (T (u)) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n)$
34		simplll	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (N \in Fin \land R \in Ring)$
35	28	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \to u \in B$
36	35	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (u \in B \land n \in ℕ_{0})$
37	1 2 3 4 5 6 7 8	pm2mpf1lem	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land n \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n) = u decompPMat n$
38	34 36 37	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((u decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n) = u decompPMat n$
39	33 38	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (T (u)) (n) = u decompPMat n$
40		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to w \in B$
41	1 2 3 4 5 6 7 8 9	pm2mpfval	$⊢ (N \in Fin \land R \in Ring \land w \in B) \to T (w) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
42	26 27 40 41	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to T (w) = \underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))$
43	42	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to {coe}_{1} (T (w)) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X)))$
44	43	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to {coe}_{1} (T (w)) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n)$
45	44	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (T (w)) (n) = {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n)$
46	40	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \to w \in B$
47	46	anim1i	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (w \in B \land n \in ℕ_{0})$
48	1 2 3 4 5 6 7 8	pm2mpf1lem	$⊢ ((N \in Fin \land R \in Ring) \land (w \in B \land n \in ℕ_{0})) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n) = w decompPMat n$
49	34 47 48	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (\underset{k \in ℕ_{0}}{\sum_{Q}} ((w decompPMat k) \underset{˙}{*} (k \underset{˙}{\times} X))) (n) = w decompPMat n$
50	45 49	eqtrd	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to {coe}_{1} (T (w)) (n) = w decompPMat n$
51	39 50	eqeq12d	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to ({coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n) \leftrightarrow u decompPMat n = w decompPMat n)$
52	2 3	decpmatval	$⊢ (u \in B \land n \in ℕ_{0}) \to u decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n))$
53	28 52	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to u decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n))$
54	2 3	decpmatval	$⊢ (w \in B \land n \in ℕ_{0}) \to w decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n))$
55	40 54	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to w decompPMat n = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n))$
56	53 55	eqeq12d	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to (u decompPMat n = w decompPMat n \leftrightarrow (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)))$
57		eqid	$⊢ {Base}_{R} = {Base}_{R}$
58		eqid	$⊢ {Base}_{A} = {Base}_{A}$
59		simplll	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to N \in Fin$
60		simpllr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to R \in Ring$
61		eqid	$⊢ {Base}_{P} = {Base}_{P}$
62		simp2	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
63		simp3	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
64	3	eleq2i	$⊢ u \in B \leftrightarrow u \in {Base}_{C}$
65	64	birani	$⊢ (u \in B \land w \in B) \to u \in {Base}_{C}$
66	65	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to u \in {Base}_{C}$
67	66	3ad2ant1	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to u \in {Base}_{C}$
68	67 3	eleqtrrdi	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to u \in B$
69	2 61 3 62 63 68	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i u j \in {Base}_{P}$
70		simp1r	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to n \in ℕ_{0}$
71		eqid	$⊢ {coe}_{1} (i u j) = {coe}_{1} (i u j)$
72	71 61 1 57	coe1fvalcl	$⊢ (i u j \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (i u j) (n) \in {Base}_{R}$
73	69 70 72	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i u j) (n) \in {Base}_{R}$
74	7 57 58 59 60 73	matbas2d	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) \in {Base}_{A}$
75	3	eleq2i	$⊢ w \in B \leftrightarrow w \in {Base}_{C}$
76	75	biimpi	$⊢ w \in B \to w \in {Base}_{C}$
77	76	ad2antll	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to w \in {Base}_{C}$
78	77	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to w \in {Base}_{C}$
79	78	3ad2ant1	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to w \in {Base}_{C}$
80	79 3	eleqtrrdi	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to w \in B$
81	2 61 3 62 63 80	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i w j \in {Base}_{P}$
82		eqid	$⊢ {coe}_{1} (i w j) = {coe}_{1} (i w j)$
83	82 61 1 57	coe1fvalcl	$⊢ (i w j \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (i w j) (n) \in {Base}_{R}$
84	81 70 83	syl2anc	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to {coe}_{1} (i w j) (n) \in {Base}_{R}$
85	7 57 58 59 60 84	matbas2d	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) \in {Base}_{A}$
86	7 58	eqmat	$⊢ ((i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) \in {Base}_{A} \land (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) \in {Base}_{A}) \to ((i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y)$
87	74 85 86	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to ((i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y)$
88	56 87	bitrd	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land n \in ℕ_{0}) \to (u decompPMat n = w decompPMat n \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y)$
89	88	adantlr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (u decompPMat n = w decompPMat n \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y)$
90		oveq1	$⊢ x = a \to x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y$
91		oveq1	$⊢ x = a \to x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y$
92	90 91	eqeq12d	$⊢ x = a \to (x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \leftrightarrow a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y)$
93		oveq2	$⊢ y = b \to a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b$
94		oveq2	$⊢ y = b \to a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b$
95	93 94	eqeq12d	$⊢ y = b \to (a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \leftrightarrow a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b)$
96	92 95	rspc2va	$⊢ ((a \in N \land b \in N) \land \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y) \to a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b$
97		eqidd	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) = (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n))$
98		oveq12	$⊢ (i = a \land j = b) \to i u j = a u b$
99	98	fveq2d	$⊢ (i = a \land j = b) \to {coe}_{1} (i u j) = {coe}_{1} (a u b)$
100	99	fveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i u j) (n) = {coe}_{1} (a u b) (n)$
101	100	adantl	$⊢ ((((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \land (i = a \land j = b)) \to {coe}_{1} (i u j) (n) = {coe}_{1} (a u b) (n)$
102		simplll	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to a \in N$
103		simpllr	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to b \in N$
104		fvexd	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to {coe}_{1} (a u b) (n) \in V$
105	97 101 102 103 104	ovmpod	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = {coe}_{1} (a u b) (n)$
106		eqidd	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) = (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n))$
107		oveq12	$⊢ (i = a \land j = b) \to i w j = a w b$
108	107	fveq2d	$⊢ (i = a \land j = b) \to {coe}_{1} (i w j) = {coe}_{1} (a w b)$
109	108	fveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i w j) (n) = {coe}_{1} (a w b) (n)$
110	109	adantl	$⊢ ((((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \land (i = a \land j = b)) \to {coe}_{1} (i w j) (n) = {coe}_{1} (a w b) (n)$
111		fvexd	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to {coe}_{1} (a w b) (n) \in V$
112	106 110 102 103 111	ovmpod	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b = {coe}_{1} (a w b) (n)$
113	105 112	eqeq12d	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to (a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b \leftrightarrow {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
114	113	biimpd	$⊢ (((a \in N \land b \in N) \land ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B))) \land n \in ℕ_{0}) \to (a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
115	114	exp31	$⊢ (a \in N \land b \in N) \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to (a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))))$
116	115	com14	$⊢ a (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) b = a (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) b \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to ((a \in N \land b \in N) \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))))$
117	96 116	syl	$⊢ ((a \in N \land b \in N) \land \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y) \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to ((a \in N \land b \in N) \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))))$
118	117	ex	$⊢ (a \in N \land b \in N) \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to ((a \in N \land b \in N) \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n)))))$
119	118	com25	$⊢ (a \in N \land b \in N) \to ((a \in N \land b \in N) \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n)))))$
120	119	pm2.43i	$⊢ (a \in N \land b \in N) \to (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (n \in ℕ_{0} \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))))$
121	120	impcom	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \to (n \in ℕ_{0} \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n)))$
122	121	imp	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (\forall x \in N \forall y \in N x (i \in N, j \in N ⟼ {coe}_{1} (i u j) (n)) y = x (i \in N, j \in N ⟼ {coe}_{1} (i w j) (n)) y \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
123	89 122	sylbid	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to (u decompPMat n = w decompPMat n \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
124	51 123	sylbid	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \land n \in ℕ_{0}) \to ({coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n) \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
125	124	ralimdva	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land (a \in N \land b \in N)) \to (\forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n) \to \forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
126	125	impancom	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \to ((a \in N \land b \in N) \to \forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
127	126	imp	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to \forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n)$
128	27	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to R \in Ring$
129		simprl	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to a \in N$
130		simprr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to b \in N$
131	65	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \to u \in {Base}_{C}$
132	131	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to u \in {Base}_{C}$
133	132 3	eleqtrrdi	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to u \in B$
134	2 61 3 129 130 133	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to a u b \in {Base}_{P}$
135	77	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to w \in {Base}_{C}$
136	135 3	eleqtrrdi	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to w \in B$
137	2 61 3 129 130 136	matecld	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to a w b \in {Base}_{P}$
138		eqid	$⊢ {coe}_{1} (a u b) = {coe}_{1} (a u b)$
139		eqid	$⊢ {coe}_{1} (a w b) = {coe}_{1} (a w b)$
140	1 61 138 139	ply1coe1eq	$⊢ (R \in Ring \land a u b \in {Base}_{P} \land a w b \in {Base}_{P}) \to (\forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n) \leftrightarrow a u b = a w b)$
141	140	bicomd	$⊢ (R \in Ring \land a u b \in {Base}_{P} \land a w b \in {Base}_{P}) \to (a u b = a w b \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
142	128 134 137 141	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to (a u b = a w b \leftrightarrow \forall n \in ℕ_{0} {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
143	127 142	mpbird	$⊢ ((((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \land (a \in N \land b \in N)) \to a u b = a w b$
144	143	ralrimivva	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \to \forall a \in N \forall b \in N a u b = a w b$
145	2 3	eqmat	$⊢ (u \in B \land w \in B) \to (u = w \leftrightarrow \forall a \in N \forall b \in N a u b = a w b)$
146	145	ad2antlr	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \to (u = w \leftrightarrow \forall a \in N \forall b \in N a u b = a w b)$
147	144 146	mpbird	$⊢ (((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \land \forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n)) \to u = w$
148	147	ex	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (\forall n \in ℕ_{0} {coe}_{1} (T (u)) (n) = {coe}_{1} (T (w)) (n) \to u = w)$
149	25 148	sylbid	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (T (u) = T (w) \to u = w)$
150	149	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall u \in B \forall w \in B (T (u) = T (w) \to u = w)$
151		dff13	$⊢ T : B \underset{1-1}{⟶} L \leftrightarrow (T : B ⟶ L \land \forall u \in B \forall w \in B (T (u) = T (w) \to u = w))$
152	11 150 151	sylanbrc	$⊢ (N \in Fin \land R \in Ring) \to T : B \underset{1-1}{⟶} L$

Metamath Proof Explorer

Theorem pm2mpf1

Proof