| Step | Hyp | Ref
| Expression |
| 1 | | decpmatid.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
| 2 | | decpmatid.c |
. . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) |
| 3 | 1, 2 | pmatring 22698 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
| 4 | 3 | 3adant3 1133 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝐶 ∈
Ring) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 6 | | decpmatid.i |
. . . . 5
⊢ 𝐼 = (1r‘𝐶) |
| 7 | 5, 6 | ringidcl 20262 |
. . . 4
⊢ (𝐶 ∈ Ring → 𝐼 ∈ (Base‘𝐶)) |
| 8 | 4, 7 | syl 17 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝐼 ∈
(Base‘𝐶)) |
| 9 | | simp3 1139 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝐾 ∈
ℕ0) |
| 10 | 2, 5 | decpmatval 22771 |
. . 3
⊢ ((𝐼 ∈ (Base‘𝐶) ∧ 𝐾 ∈ ℕ0) → (𝐼 decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝐼𝑗))‘𝐾))) |
| 11 | 8, 9, 10 | syl2anc 584 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (𝐼 decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝐼𝑗))‘𝐾))) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑃) = (1r‘𝑃) |
| 14 | | simp11 1204 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑁 ∈ Fin) |
| 15 | | simp12 1205 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring) |
| 16 | | simp2 1138 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
| 17 | | simp3 1139 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
| 18 | 1, 2, 12, 13, 14, 15, 16, 17, 6 | pmat1ovd 22703 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝐼𝑗) = if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃))) |
| 19 | 18 | fveq2d 6910 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (coe1‘(𝑖𝐼𝑗)) = (coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃)))) |
| 20 | 19 | fveq1d 6908 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝐼𝑗))‘𝐾) = ((coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃)))‘𝐾)) |
| 21 | | fvif 6922 |
. . . . . . 7
⊢
(coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃))) = if(𝑖 = 𝑗,
(coe1‘(1r‘𝑃)),
(coe1‘(0g‘𝑃))) |
| 22 | 21 | fveq1i 6907 |
. . . . . 6
⊢
((coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃)))‘𝐾) = (if(𝑖 = 𝑗,
(coe1‘(1r‘𝑃)),
(coe1‘(0g‘𝑃)))‘𝐾) |
| 23 | | iffv 6923 |
. . . . . 6
⊢ (if(𝑖 = 𝑗,
(coe1‘(1r‘𝑃)),
(coe1‘(0g‘𝑃)))‘𝐾) = if(𝑖 = 𝑗,
((coe1‘(1r‘𝑃))‘𝐾),
((coe1‘(0g‘𝑃))‘𝐾)) |
| 24 | 22, 23 | eqtri 2765 |
. . . . 5
⊢
((coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃)))‘𝐾) = if(𝑖 = 𝑗,
((coe1‘(1r‘𝑃))‘𝐾),
((coe1‘(0g‘𝑃))‘𝐾)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(var1‘𝑅) = (var1‘𝑅) |
| 26 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 27 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
| 28 | 1, 25, 26, 27 | ply1idvr1 22298 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (1r‘𝑃)) |
| 29 | 28 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (1r‘𝑃)) |
| 30 | 29 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (1r‘𝑃) =
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
| 31 | 30 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (coe1‘(1r‘𝑃)) =
(coe1‘(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
| 32 | 31 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘(1r‘𝑃))‘𝐾) =
((coe1‘(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝐾)) |
| 33 | 1 | ply1lmod 22253 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
| 34 | 33 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝑃 ∈
LMod) |
| 35 | | 0nn0 12541 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 37 | 1, 25, 26, 27, 36 | ply1moncl 22274 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 0 ∈
ℕ0) → (0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
| 38 | 35, 37 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
| 39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
| 42 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘(Scalar‘𝑃)) =
(1r‘(Scalar‘𝑃)) |
| 43 | 36, 40, 41, 42 | lmodvs1 20888 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ LMod ∧
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) →
((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
| 44 | 34, 39, 43 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
| 45 | 44 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (0(.g‘(mulGrp‘𝑃))(var1‘𝑅)) =
((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (coe1‘(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(coe1‘((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
| 47 | 46 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))‘𝐾) =
((coe1‘((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝐾)) |
| 48 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝑅 ∈
Ring) |
| 49 | 1 | ply1sca 22254 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
| 50 | 49 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 𝑅 =
(Scalar‘𝑃)) |
| 51 | 50 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (Scalar‘𝑃) =
𝑅) |
| 52 | 51 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (1r‘(Scalar‘𝑃)) = (1r‘𝑅)) |
| 53 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 55 | 53, 54 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 56 | 55 | 3ad2ant2 1135 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (1r‘𝑅) ∈ (Base‘𝑅)) |
| 57 | 52, 56 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (1r‘(Scalar‘𝑃)) ∈ (Base‘𝑅)) |
| 58 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 0 ∈ ℕ0) |
| 59 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 60 | 59, 53, 1, 25, 41, 26, 27 | coe1tm 22276 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
(1r‘(Scalar‘𝑃)) ∈ (Base‘𝑅) ∧ 0 ∈ ℕ0) →
(coe1‘((1r‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)))) |
| 61 | 48, 57, 58, 60 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (coe1‘((1r‘(Scalar‘𝑃))(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (𝑘 ∈ ℕ0 ↦ if(𝑘 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)))) |
| 62 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑘 = 0 ↔ 𝐾 = 0)) |
| 63 | 62 | ifbid 4549 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → if(𝑘 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) = if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 64 | 63 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑘 = 𝐾) → if(𝑘 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) = if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 65 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(1r‘(Scalar‘𝑃)) ∈ V |
| 66 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
| 67 | 65, 66 | ifex 4576 |
. . . . . . . . . 10
⊢ if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) ∈ V |
| 68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) ∈ V) |
| 69 | 61, 64, 9, 68 | fvmptd 7023 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘((1r‘(Scalar‘𝑃))(
·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝐾) = if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 70 | 32, 47, 69 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘(1r‘𝑃))‘𝐾) = if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 71 | 1, 12, 59 | coe1z 22266 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
| 72 | 71 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
| 73 | 72 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘(0g‘𝑃))‘𝐾) = ((ℕ0 ×
{(0g‘𝑅)})‘𝐾)) |
| 74 | 66 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (0g‘𝑅) ∈ V) |
| 75 | | fvconst2g 7222 |
. . . . . . . . 9
⊢
(((0g‘𝑅) ∈ V ∧ 𝐾 ∈ ℕ0) →
((ℕ0 × {(0g‘𝑅)})‘𝐾) = (0g‘𝑅)) |
| 76 | 74, 9, 75 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((ℕ0 × {(0g‘𝑅)})‘𝐾) = (0g‘𝑅)) |
| 77 | 73, 76 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ ((coe1‘(0g‘𝑃))‘𝐾) = (0g‘𝑅)) |
| 78 | 70, 77 | ifeq12d 4547 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ if(𝑖 = 𝑗,
((coe1‘(1r‘𝑃))‘𝐾),
((coe1‘(0g‘𝑃))‘𝐾)) = if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) |
| 79 | 78 | 3ad2ant1 1134 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → if(𝑖 = 𝑗,
((coe1‘(1r‘𝑃))‘𝐾),
((coe1‘(0g‘𝑃))‘𝐾)) = if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) |
| 80 | 24, 79 | eqtrid 2789 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘if(𝑖 = 𝑗, (1r‘𝑃), (0g‘𝑃)))‘𝐾) = if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) |
| 81 | 20, 80 | eqtrd 2777 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((coe1‘(𝑖𝐼𝑗))‘𝐾) = if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) |
| 82 | 81 | mpoeq3dva 7510 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑖𝐼𝑗))‘𝐾)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅)))) |
| 83 | 50 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → 𝑅 = (Scalar‘𝑃)) |
| 84 | 83 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) →
(Scalar‘𝑃) = 𝑅) |
| 85 | 84 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) →
(1r‘(Scalar‘𝑃)) = (1r‘𝑅)) |
| 86 | 85 | ifeq1d 4545 |
. . . . . 6
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) →
if(𝑖 = 𝑗, (1r‘(Scalar‘𝑃)), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅))) |
| 87 | 86 | mpoeq3dv 7512 |
. . . . 5
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘(Scalar‘𝑃)), (0g‘𝑅))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))) |
| 88 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝐾 = 0 → if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) =
(1r‘(Scalar‘𝑃))) |
| 89 | 88 | ifeq1d 4545 |
. . . . . . 7
⊢ (𝐾 = 0 → if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 90 | 89 | adantr 480 |
. . . . . 6
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) →
if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅)) = if(𝑖 = 𝑗, (1r‘(Scalar‘𝑃)), (0g‘𝑅))) |
| 91 | 90 | mpoeq3dv 7512 |
. . . . 5
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘(Scalar‘𝑃)), (0g‘𝑅)))) |
| 92 | | decpmatid.1 |
. . . . . . . 8
⊢ 1 =
(1r‘𝐴) |
| 93 | | decpmatid.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 94 | 93, 54, 59 | mat1 22453 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))) |
| 95 | 92, 94 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))) |
| 96 | 95 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ 1
= (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))) |
| 97 | 96 | adantl 481 |
. . . . 5
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → 1 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (1r‘𝑅), (0g‘𝑅)))) |
| 98 | 87, 91, 97 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = 1 ) |
| 99 | | iftrue 4531 |
. . . . . 6
⊢ (𝐾 = 0 → if(𝐾 = 0, 1 , 0 ) = 1 ) |
| 100 | 99 | eqcomd 2743 |
. . . . 5
⊢ (𝐾 = 0 → 1 = if(𝐾 = 0, 1 , 0 )) |
| 101 | 100 | adantr 480 |
. . . 4
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → 1 = if(𝐾 = 0, 1 , 0 )) |
| 102 | 98, 101 | eqtrd 2777 |
. . 3
⊢ ((𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = if(𝐾 = 0, 1 , 0 )) |
| 103 | | ifid 4566 |
. . . . . . 7
⊢ if(𝑖 = 𝑗, (0g‘𝑅), (0g‘𝑅)) = (0g‘𝑅) |
| 104 | 103 | a1i 11 |
. . . . . 6
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ if(𝑖 = 𝑗, (0g‘𝑅), (0g‘𝑅)) = (0g‘𝑅)) |
| 105 | 104 | mpoeq3dv 7512 |
. . . . 5
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (0g‘𝑅), (0g‘𝑅))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
| 106 | | iffalse 4534 |
. . . . . . . 8
⊢ (¬
𝐾 = 0 → if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) = (0g‘𝑅)) |
| 107 | 106 | adantr 480 |
. . . . . . 7
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)) = (0g‘𝑅)) |
| 108 | 107 | ifeq1d 4545 |
. . . . . 6
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅)) = if(𝑖 = 𝑗, (0g‘𝑅), (0g‘𝑅))) |
| 109 | 108 | mpoeq3dv 7512 |
. . . . 5
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (0g‘𝑅), (0g‘𝑅)))) |
| 110 | | 3simpa 1149 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (𝑁 ∈ Fin ∧
𝑅 ∈
Ring)) |
| 111 | 110 | adantl 481 |
. . . . . 6
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ (𝑁 ∈ Fin ∧
𝑅 ∈
Ring)) |
| 112 | | decpmatid.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝐴) |
| 113 | 93, 59 | mat0op 22425 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
| 114 | 112, 113 | eqtrid 2789 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
| 115 | 111, 114 | syl 17 |
. . . . 5
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ 0
= (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (0g‘𝑅))) |
| 116 | 105, 109,
115 | 3eqtr4d 2787 |
. . . 4
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = 0 ) |
| 117 | | iffalse 4534 |
. . . . . 6
⊢ (¬
𝐾 = 0 → if(𝐾 = 0, 1 , 0 ) = 0 ) |
| 118 | 117 | eqcomd 2743 |
. . . . 5
⊢ (¬
𝐾 = 0 → 0 = if(𝐾 = 0, 1 , 0 )) |
| 119 | 118 | adantr 480 |
. . . 4
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ 0
= if(𝐾 = 0, 1 , 0
)) |
| 120 | 116, 119 | eqtrd 2777 |
. . 3
⊢ ((¬
𝐾 = 0 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0))
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = if(𝐾 = 0, 1 , 0 )) |
| 121 | 102, 120 | pm2.61ian 812 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, if(𝐾 = 0,
(1r‘(Scalar‘𝑃)), (0g‘𝑅)), (0g‘𝑅))) = if(𝐾 = 0, 1 , 0 )) |
| 122 | 11, 82, 121 | 3eqtrd 2781 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐾 ∈ ℕ0)
→ (𝐼 decompPMat 𝐾) = if(𝐾 = 0, 1 , 0 )) |