Step | Hyp | Ref
| Expression |
1 | | minmar1fval.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | minmar1fval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐴) |
3 | | minmar1fval.q |
. . . . 5
⊢ 𝑄 = (𝑁 minMatR1 𝑅) |
4 | | minmar1fval.o |
. . . . 5
⊢ 1 =
(1r‘𝑅) |
5 | | minmar1fval.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
6 | 1, 2, 3, 4, 5 | minmar1val 20273 |
. . . 4
⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))) |
7 | 6 | 3expb 1258 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))) |
8 | 7 | 3adant3 1074 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))) |
9 | | simp3l 1082 |
. . 3
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝐼 ∈ 𝑁) |
10 | | simpl3r 1110 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) ∧ 𝑖 = 𝐼) → 𝐽 ∈ 𝑁) |
11 | | fvex 6113 |
. . . . . . 7
⊢
(1r‘𝑅) ∈ V |
12 | 4, 11 | eqeltri 2684 |
. . . . . 6
⊢ 1 ∈
V |
13 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
14 | 5, 13 | eqeltri 2684 |
. . . . . 6
⊢ 0 ∈
V |
15 | 12, 14 | ifex 4106 |
. . . . 5
⊢ if(𝑗 = 𝐿, 1 , 0 ) ∈
V |
16 | | ovex 6577 |
. . . . 5
⊢ (𝑖𝑀𝑗) ∈ V |
17 | 15, 16 | ifex 4106 |
. . . 4
⊢ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)) ∈ V |
18 | 17 | a1i 11 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)) ∈ V) |
19 | | eqeq1 2614 |
. . . . . 6
⊢ (𝑖 = 𝐼 → (𝑖 = 𝐾 ↔ 𝐼 = 𝐾)) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑗 = 𝐽) → (𝑖 = 𝐾 ↔ 𝐼 = 𝐾)) |
21 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (𝑗 = 𝐿 ↔ 𝐽 = 𝐿)) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑗 = 𝐽) → (𝑗 = 𝐿 ↔ 𝐽 = 𝐿)) |
23 | 22 | ifbid 4058 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑗 = 𝐽) → if(𝑗 = 𝐿, 1 , 0 ) = if(𝐽 = 𝐿, 1 , 0 )) |
24 | | oveq12 6558 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑗 = 𝐽) → (𝑖𝑀𝑗) = (𝐼𝑀𝐽)) |
25 | 20, 23, 24 | ifbieq12d 4063 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑗 = 𝐽) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽))) |
26 | 25 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽))) |
27 | 9, 10, 18, 26 | ovmpt2dv2 6692 |
. 2
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗))) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽)))) |
28 | 8, 27 | mpd 15 |
1
⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽))) |