Step | Hyp | Ref
| Expression |
1 | | minmar1fval.q |
. 2
⊢ 𝑄 = (𝑁 minMatR1 𝑅) |
2 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
3 | | minmar1fval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = 𝐴) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘𝐴)) |
6 | | minmar1fval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
7 | 5, 6 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
8 | | simpl 472 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
9 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = (1r‘𝑅)) |
10 | | minmar1fval.o |
. . . . . . . . . . 11
⊢ 1 =
(1r‘𝑅) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (1r‘𝑟) = 1 ) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
13 | | minmar1fval.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
15 | 11, 14 | ifeq12d 4056 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)) = if(𝑗 = 𝑙, 1 , 0 )) |
16 | 15 | ifeq1d 4054 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)) = if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)) = if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))) |
18 | 8, 8, 17 | mpt2eq123dv 6615 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))) |
19 | 8, 8, 18 | mpt2eq123dv 6615 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) |
20 | 7, 19 | mpteq12dv 4663 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))) = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))) |
21 | | df-minmar1 20260 |
. . . 4
⊢ minMatR1
= (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))))) |
22 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐴)
∈ V |
23 | 6, 22 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
24 | 23 | mptex 6390 |
. . . 4
⊢ (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) ∈ V |
25 | 20, 21, 24 | ovmpt2a 6689 |
. . 3
⊢ ((𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 minMatR1 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))) |
26 | 21 | mpt2ndm0 6773 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 minMatR1 𝑅) = ∅) |
27 | | mpt0 5934 |
. . . . 5
⊢ (𝑚 ∈ ∅ ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) = ∅ |
28 | 26, 27 | syl6eqr 2662 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 minMatR1 𝑅) = (𝑚 ∈ ∅ ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))) |
29 | 3 | fveq2i 6106 |
. . . . . . 7
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
30 | 6, 29 | eqtri 2632 |
. . . . . 6
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
31 | | matbas0pc 20034 |
. . . . . 6
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) →
(Base‘(𝑁 Mat 𝑅)) = ∅) |
32 | 30, 31 | syl5eq 2656 |
. . . . 5
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → 𝐵 = ∅) |
33 | 32 | mpteq1d 4666 |
. . . 4
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) = (𝑚 ∈ ∅ ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))) |
34 | 28, 33 | eqtr4d 2647 |
. . 3
⊢ (¬
(𝑁 ∈ V ∧ 𝑅 ∈ V) → (𝑁 minMatR1 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))) |
35 | 25, 34 | pm2.61i 175 |
. 2
⊢ (𝑁 minMatR1 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) |
36 | 1, 35 | eqtri 2632 |
1
⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) |