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 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→ 𝐿 )