Step | Hyp | Ref
| Expression |
1 | | marrepfval.q |
. 2
⊢ 𝑄 = (𝑁 matRRep 𝑅) |
2 | | marrepfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
3 | 2 | fvexi 6731 |
. . . . 5
⊢ 𝐵 ∈ V |
4 | | fvexd 6732 |
. . . . 5
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
5 | | mpoexga 7848 |
. . . . 5
⊢ ((𝐵 ∈ V ∧
(Base‘𝑅) ∈ V)
→ (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) ∈ V) |
6 | 3, 4, 5 | sylancr 590 |
. . . 4
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) ∈ V) |
7 | | oveq12 7222 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
8 | 7 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅))) |
9 | | marrepfval.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
10 | 9 | fveq2i 6720 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
11 | 2, 10 | eqtri 2765 |
. . . . . . 7
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
12 | 8, 11 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
13 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
14 | 13 | adantl 485 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘𝑟) = (Base‘𝑅)) |
15 | | simpl 486 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
16 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
17 | | marrepfval.z |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
18 | 16, 17 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
19 | 18 | ifeq2d 4459 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)) = if(𝑗 = 𝑙, 𝑠, 0 )) |
20 | 19 | ifeq1d 4458 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)) = if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))) |
21 | 20 | adantl 485 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)) = if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))) |
22 | 15, 15, 21 | mpoeq123dv 7286 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))) |
23 | 15, 15, 22 | mpoeq123dv 7286 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) |
24 | 12, 14, 23 | mpoeq123dv 7286 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))) = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))))) |
25 | | df-marrep 21455 |
. . . . 5
⊢ matRRep
= (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)))))) |
26 | 24, 25 | ovmpoga 7363 |
. . . 4
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V ∧ (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) ∈ V) → (𝑁 matRRep 𝑅) = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))))) |
27 | 6, 26 | mpd3an3 1464 |
. . 3
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 matRRep 𝑅) = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))))) |
28 | 25 | mpondm0 7446 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 matRRep 𝑅) = ∅) |
29 | | matbas0pc 21306 |
. . . . . . 7
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) →
(Base‘(𝑁 Mat 𝑅)) = ∅) |
30 | 11, 29 | syl5eq 2790 |
. . . . . 6
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
31 | 30 | orcd 873 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝐵 = ∅ ∨
(Base‘𝑅) =
∅)) |
32 | | 0mpo0 7294 |
. . . . 5
⊢ ((𝐵 = ∅ ∨
(Base‘𝑅) = ∅)
→ (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) = ∅) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) = ∅) |
34 | 28, 33 | eqtr4d 2780 |
. . 3
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 matRRep 𝑅) = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))))) |
35 | 27, 34 | pm2.61i 185 |
. 2
⊢ (𝑁 matRRep 𝑅) = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) |
36 | 1, 35 | eqtri 2765 |
1
⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) |