Theorem 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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
	pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
	pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
	pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
	pm2mpcl.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
Assertion	pm2mpf1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpval.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		pm2mpval.m	⊢ ∗ = ( ·𝑠 ‘ 𝑄 )
5		pm2mpval.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
6		pm2mpval.x	⊢ 𝑋 = ( var1 ‘ 𝐴 )
7		pm2mpval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
8		pm2mpval.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
9		pm2mpval.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
10		pm2mpcl.l	⊢ 𝐿 = ( Base ‘ 𝑄 )
11	1 2 3 4 5 6 7 8 9 10	pm2mpf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐿 )
12	7	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
13	12	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐴 ∈ Ring )
14	1 2 3 4 5 6 7 8 9 10	pm2mpcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑢 ) ∈ 𝐿 )
15	14	3expa	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑢 ) ∈ 𝐿 )
16	15	adantrr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑢 ) ∈ 𝐿 )
17	1 2 3 4 5 6 7 8 9 10	pm2mpcl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 )
18	17	3expia	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑤 ∈ 𝐵 → ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 ) )
19	18	adantld	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 ) )
20	19	imp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 )
21		eqid	⊢ ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) = ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) )
22		eqid	⊢ ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) = ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) )
23	8 10 21 22	ply1coe1eq	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑇 ‘ 𝑢 ) ∈ 𝐿 ∧ ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ↔ ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) ) )
24	23	bicomd	⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝑇 ‘ 𝑢 ) ∈ 𝐿 ∧ ( 𝑇 ‘ 𝑤 ) ∈ 𝐿 ) → ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) )
25	13 16 20 24	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) )
26		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
27		simplr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
28		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
29	1 2 3 4 5 6 7 8 9	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑢 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
30	26 27 28 29	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑢 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
31	30	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ 𝑢 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
32	31	fveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
33	32	fveq1d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
34		simplll	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
35	28	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑢 ∈ 𝐵 )
36	35	anim1i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑢 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) )
37	1 2 3 4 5 6 7 8	pm2mpf1lem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝑢 decompPMat 𝑛 ) )
38	34 36 37	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑢 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝑢 decompPMat 𝑛 ) )
39	33 38	eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( 𝑢 decompPMat 𝑛 ) )
40		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
41	1 2 3 4 5 6 7 8 9	pm2mpfval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑤 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
42	26 27 40 41	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑤 ) = ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
43	42	fveq2d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) = ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
44	43	fveq1d	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
45	44	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) )
46	40	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑤 ∈ 𝐵 )
47	46	anim1i	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑤 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) )
48	1 2 3 4 5 6 7 8	pm2mpf1lem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) )
49	34 47 48	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑄 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑤 decompPMat 𝑘 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) )
50	45 49	eqtrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) )
51	39 50	eqeq12d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ↔ ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ) )
52	2 3	decpmatval	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑢 decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) )
53	28 52	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑢 decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) )
54	2 3	decpmatval	⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑤 decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) )
55	40 54	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑤 decompPMat 𝑛 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) )
56	53 55	eqeq12d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ↔ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ) )
57		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
58		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
59		simplll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
60		simpllr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
61		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
62		simp2	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
63		simp3	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
64	3	eleq2i	⊢ ( 𝑢 ∈ 𝐵 ↔ 𝑢 ∈ ( Base ‘ 𝐶 ) )
65	64	biimpi	⊢ ( 𝑢 ∈ 𝐵 → 𝑢 ∈ ( Base ‘ 𝐶 ) )
66	65	adantr	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
67	66	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
68	67	3ad2ant1	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
69	68 3	eleqtrrdi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑢 ∈ 𝐵 )
70	2 61 3 62 63 69	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑢 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
71		simp1r	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑛 ∈ ℕ0 )
72		eqid	⊢ ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) )
73	72 61 1 57	coe1fvalcl	⊢ ( ( ( 𝑖 𝑢 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
74	70 71 73	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
75	7 57 58 59 60 74	matbas2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) )
76	3	eleq2i	⊢ ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ( Base ‘ 𝐶 ) )
77	76	biimpi	⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( Base ‘ 𝐶 ) )
78	77	ad2antll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
79	78	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
80	79	3ad2ant1	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
81	80 3	eleqtrrdi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑤 ∈ 𝐵 )
82	2 61 3 62 63 81	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑤 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
83		eqid	⊢ ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) )
84	83 61 1 57	coe1fvalcl	⊢ ( ( ( 𝑖 𝑤 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
85	82 71 84	syl2anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
86	7 57 58 59 60 85	matbas2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) )
87	7 58	eqmat	⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
88	75 86 87	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
89	56 88	bitrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
90	89	adantlr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
91		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) )
92		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) )
93	91 92	eqeq12d	⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ↔ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
94		oveq2	⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
95		oveq2	⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
96	94 95	eqeq12d	⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ↔ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) ) )
97	93 96	rspc2va	⊢ ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
98		eqidd	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) )
99		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 𝑢 𝑗 ) = ( 𝑎 𝑢 𝑏 ) )
100	99	fveq2d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) = ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) )
101	100	fveq1d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
102	101	adantl	⊢ ( ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
103		simplll	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑎 ∈ 𝑁 )
104		simpllr	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑏 ∈ 𝑁 )
105		fvexd	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) ∈ V )
106	98 102 103 104 105	ovmpod	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
107		eqidd	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) )
108		oveq12	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 𝑤 𝑗 ) = ( 𝑎 𝑤 𝑏 ) )
109	108	fveq2d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) = ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) )
110	109	fveq1d	⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
111	110	adantl	⊢ ( ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
112		fvexd	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ∈ V )
113	107 111 103 104 112	ovmpod	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
114	106 113	eqeq12d	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) ↔ ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
115	114	biimpd	⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
116	115	exp31	⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
117	116	com14	⊢ ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
118	97 117	syl	⊢ ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
119	118	ex	⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) ) )
120	119	com25	⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) ) )
121	120	pm2.43i	⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
122	121	impcom	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) )
123	122	imp	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
124	90 123	sylbid	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
125	51 124	sylbid	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
126	125	ralimdva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
127	126	impancom	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
128	127	imp	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
129	27	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
130		simprl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
131		simprr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
132	66	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
133	132	adantr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
134	133 3	eleqtrrdi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑢 ∈ 𝐵 )
135	2 61 3 130 131 134	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
136	78	ad2antrr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
137	136 3	eleqtrrdi	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑤 ∈ 𝐵 )
138	2 61 3 130 131 137	matecld	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
139		eqid	⊢ ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) = ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) )
140		eqid	⊢ ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) = ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) )
141	1 61 139 140	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ↔ ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
142	141	bicomd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
143	129 135 138 142	syl3anc	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
144	128 143	mpbird	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) )
145	144	ralrimivva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) )
146	2 3	eqmat	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 = 𝑤 ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
147	146	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ( 𝑢 = 𝑤 ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
148	145 147	mpbird	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → 𝑢 = 𝑤 )
149	148	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → 𝑢 = 𝑤 ) )
150	25 149	sylbid	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
151	150	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
152		dff13	⊢ ( 𝑇 : 𝐵 –1-1→ 𝐿 ↔ ( 𝑇 : 𝐵 ⟶ 𝐿 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) ) )
153	11 151 152	sylanbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐿 )