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	biimpi	$⊢ u \in B \to u \in {Base}_{C}$
66	65	adantr	$⊢ (u \in B \land w \in B) \to u \in {Base}_{C}$
67	66	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}$
68	67	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}$
69	68 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$
70	2 61 3 62 63 69	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}$
71		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}$
72		eqid	$⊢ {coe}_{1} (i u j) = {coe}_{1} (i u j)$
73	72 61 1 57	coe1fvalcl	$⊢ (i u j \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (i u j) (n) \in {Base}_{R}$
74	70 71 73	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}$
75	7 57 58 59 60 74	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}$
76	3	eleq2i	$⊢ w \in B \leftrightarrow w \in {Base}_{C}$
77	76	biimpi	$⊢ w \in B \to w \in {Base}_{C}$
78	77	ad2antll	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to w \in {Base}_{C}$
79	78	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}$
80	79	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}$
81	80 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$
82	2 61 3 62 63 81	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}$
83		eqid	$⊢ {coe}_{1} (i w j) = {coe}_{1} (i w j)$
84	83 61 1 57	coe1fvalcl	$⊢ (i w j \in {Base}_{P} \land n \in ℕ_{0}) \to {coe}_{1} (i w j) (n) \in {Base}_{R}$
85	82 71 84	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}$
86	7 57 58 59 60 85	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}$
87	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)$
88	75 86 87	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)$
89	56 88	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)$
90	89	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)$
91		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$
92		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$
93	91 92	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)$
94		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$
95		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$
96	94 95	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)$
97	93 96	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$
98		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))$
99		oveq12	$⊢ (i = a \land j = b) \to i u j = a u b$
100	99	fveq2d	$⊢ (i = a \land j = b) \to {coe}_{1} (i u j) = {coe}_{1} (a u b)$
101	100	fveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i u j) (n) = {coe}_{1} (a u b) (n)$
102	101	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)$
103		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$
104		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$
105		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$
106	98 102 103 104 105	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)$
107		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))$
108		oveq12	$⊢ (i = a \land j = b) \to i w j = a w b$
109	108	fveq2d	$⊢ (i = a \land j = b) \to {coe}_{1} (i w j) = {coe}_{1} (a w b)$
110	109	fveq1d	$⊢ (i = a \land j = b) \to {coe}_{1} (i w j) (n) = {coe}_{1} (a w b) (n)$
111	110	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)$
112		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$
113	107 111 103 104 112	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)$
114	106 113	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))$
115	114	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))$
116	115	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))))$
117	116	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))))$
118	97 117	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))))$
119	118	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)))))$
120	119	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)))))$
121	120	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))))$
122	121	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)))$
123	122	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))$
124	90 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 (u decompPMat n = w decompPMat n \to {coe}_{1} (a u b) (n) = {coe}_{1} (a w b) (n))$
125	51 124	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))$
126	125	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))$
127	126	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))$
128	127	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)$
129	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$
130		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$
131		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$
132	66	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}$
133	132	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}$
134	133 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$
135	2 61 3 130 131 134	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}$
136	78	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}$
137	136 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$
138	2 61 3 130 131 137	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}$
139		eqid	$⊢ {coe}_{1} (a u b) = {coe}_{1} (a u b)$
140		eqid	$⊢ {coe}_{1} (a w b) = {coe}_{1} (a w b)$
141	1 61 139 140	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)$
142	141	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))$
143	129 135 138 142	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))$
144	128 143	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$
145	144	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$
146	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)$
147	146	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)$
148	145 147	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$
149	148	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)$
150	25 149	sylbid	$⊢ ((N \in Fin \land R \in Ring) \land (u \in B \land w \in B)) \to (T (u) = T (w) \to u = w)$
151	150	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall u \in B \forall w \in B (T (u) = T (w) \to u = w)$
152		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))$
153	11 151 152	sylanbrc	$⊢ (N \in Fin \land R \in Ring) \to T : B \underset{1-1}{⟶} L$

Metamath Proof Explorer

Theorem pm2mpf1

Proof