Metamath Proof Explorer

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 birani ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
66 65 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
67 66 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
68 67 3 eleqtrrdi ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑢 ∈ 𝐵 )
69 2 61 3 62 63 68 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑢 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
70 simp1r ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑛 ∈ ℕ0 )
71 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) )
72 71 61 1 57 coe1fvalcl ⊢ ( ( ( 𝑖 𝑢 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
73 69 70 72 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
74 7 57 58 59 60 73 matbas2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) )
75 3 eleq2i ⊢ ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ( Base ‘ 𝐶 ) )
76 75 biimpi ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( Base ‘ 𝐶 ) )
77 76 ad2antll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
78 77 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
79 78 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
80 79 3 eleqtrrdi ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑤 ∈ 𝐵 )
81 2 61 3 62 63 80 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑤 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
82 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) )
83 82 61 1 57 coe1fvalcl ⊢ ( ( ( 𝑖 𝑤 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
84 81 70 83 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ∈ ( Base ‘ 𝑅 ) )
85 7 57 58 59 60 84 matbas2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) )
86 7 58 eqmat ⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
87 74 85 86 syl2anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
88 56 87 bitrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
89 88 adantlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
90 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) )
91 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) )
92 90 91 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ↔ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) )
93 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
94 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
95 93 94 eqeq12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ↔ ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) ) )
96 92 95 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) )
97 eqidd ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) )
98 oveq12 ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 𝑢 𝑗 ) = ( 𝑎 𝑢 𝑏 ) )
99 98 fveq2d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) = ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) )
100 99 fveq1d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
101 100 adantl ⊢ ( ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
102 simplll ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑎 ∈ 𝑁 )
103 simpllr ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑏 ∈ 𝑁 )
104 fvexd ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) ∈ V )
105 97 101 102 103 104 ovmpod ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) )
106 eqidd ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) )
107 oveq12 ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( 𝑖 𝑤 𝑗 ) = ( 𝑎 𝑤 𝑏 ) )
108 107 fveq2d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) = ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) )
109 108 fveq1d ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
110 109 adantl ⊢ ( ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) ) → ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
111 fvexd ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ∈ V )
112 106 110 102 103 111 ovmpod ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
113 105 112 eqeq12d ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) ↔ ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
114 113 biimpd ⊢ ( ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
115 114 exp31 ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
116 115 com14 ⊢ ( ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) = ( 𝑎 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑏 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
117 96 116 syl ⊢ ( ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
118 117 ex ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) ) )
119 118 com25 ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) ) )
120 119 pm2.43i ⊢ ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) ) )
121 120 impcom ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) ) )
122 121 imp ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑢 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) = ( 𝑥 ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑤 𝑗 ) ) ‘ 𝑛 ) ) 𝑦 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
123 89 122 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑢 decompPMat 𝑛 ) = ( 𝑤 decompPMat 𝑛 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
124 51 123 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
125 124 ralimdva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
126 125 impancom ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ( ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
127 126 imp ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) )
128 27 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
129 simprl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑎 ∈ 𝑁 )
130 simprr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑏 ∈ 𝑁 )
131 65 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
132 131 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑢 ∈ ( Base ‘ 𝐶 ) )
133 132 3 eleqtrrdi ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑢 ∈ 𝐵 )
134 2 61 3 129 130 133 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
135 77 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
136 135 3 eleqtrrdi ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → 𝑤 ∈ 𝐵 )
137 2 61 3 129 130 136 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
138 eqid ⊢ ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) = ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) )
139 eqid ⊢ ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) = ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) )
140 1 61 138 139 ply1coe1eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ↔ ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
141 140 bicomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑎 𝑢 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑎 𝑤 𝑏 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
142 128 134 137 141 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ↔ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑎 𝑢 𝑏 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑎 𝑤 𝑏 ) ) ‘ 𝑛 ) ) )
143 127 142 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) ∧ ( 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) ) → ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) )
144 143 ralrimivva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) )
145 2 3 eqmat ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑢 = 𝑤 ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
146 145 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → ( 𝑢 = 𝑤 ↔ ∀ 𝑎 ∈ 𝑁 ∀ 𝑏 ∈ 𝑁 ( 𝑎 𝑢 𝑏 ) = ( 𝑎 𝑤 𝑏 ) ) )
147 144 146 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) ) → 𝑢 = 𝑤 )
148 147 ex ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ∀ 𝑛 ∈ ℕ0 ( ( coe1 ‘ ( 𝑇 ‘ 𝑢 ) ) ‘ 𝑛 ) = ( ( coe1 ‘ ( 𝑇 ‘ 𝑤 ) ) ‘ 𝑛 ) → 𝑢 = 𝑤 ) )
149 25 148 sylbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
150 149 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
151 dff13 ⊢ ( 𝑇 : 𝐵 –1-1→ 𝐿 ↔ ( 𝑇 : 𝐵 ⟶ 𝐿 ∧ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ 𝑤 ) → 𝑢 = 𝑤 ) ) )
152 11 150 151 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 –1-1→ 𝐿 )