Step |
Hyp |
Ref |
Expression |
1 |
|
mdetrlin2.d |
⊢ 𝐷 = ( 𝑁 maDet 𝑅 ) |
2 |
|
mdetrlin2.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
3 |
|
mdetrlin2.p |
⊢ + = ( +g ‘ 𝑅 ) |
4 |
|
mdetrlin2.r |
⊢ ( 𝜑 → 𝑅 ∈ CRing ) |
5 |
|
mdetrlin2.n |
⊢ ( 𝜑 → 𝑁 ∈ Fin ) |
6 |
|
mdetrlin2.x |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 ) |
7 |
|
mdetrlin2.y |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 ) |
8 |
|
mdetrlin2.z |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 ) |
9 |
|
mdetrlin2.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑁 ) |
10 |
|
eqid |
⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 ) |
11 |
|
eqid |
⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) ) |
12 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
13 |
4 12
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
14 |
13
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring ) |
15 |
2 3
|
ringacl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 + 𝑌 ) ∈ 𝐾 ) |
16 |
14 6 7 15
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑋 + 𝑌 ) ∈ 𝐾 ) |
17 |
16 8
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ∈ 𝐾 ) |
18 |
10 2 11 5 4 17
|
matbas2d |
⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) |
19 |
6 8
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ∈ 𝐾 ) |
20 |
10 2 11 5 4 19
|
matbas2d |
⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) |
21 |
7 8
|
ifcld |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ∈ 𝐾 ) |
22 |
10 2 11 5 4 21
|
matbas2d |
⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ) |
23 |
|
snex |
⊢ { 𝐼 } ∈ V |
24 |
23
|
a1i |
⊢ ( 𝜑 → { 𝐼 } ∈ V ) |
25 |
9
|
snssd |
⊢ ( 𝜑 → { 𝐼 } ⊆ 𝑁 ) |
26 |
25
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐼 } ∧ 𝑗 ∈ 𝑁 ) → { 𝐼 } ⊆ 𝑁 ) |
27 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐼 } ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ { 𝐼 } ) |
28 |
26 27
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐼 } ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 ) |
29 |
28 6
|
syld3an2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐼 } ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 ) |
30 |
28 7
|
syld3an2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ { 𝐼 } ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 ) |
31 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) ) |
32 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) ) |
33 |
24 5 29 30 31 32
|
offval22 |
⊢ ( 𝜑 → ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ ( 𝑋 + 𝑌 ) ) ) |
34 |
33
|
eqcomd |
⊢ ( 𝜑 → ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ ( 𝑋 + 𝑌 ) ) = ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) ) ) |
35 |
|
mposnif |
⊢ ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ ( 𝑋 + 𝑌 ) ) |
36 |
|
mposnif |
⊢ ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) |
37 |
|
mposnif |
⊢ ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) |
38 |
36 37
|
oveq12i |
⊢ ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) = ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑋 ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ 𝑌 ) ) |
39 |
34 35 38
|
3eqtr4g |
⊢ ( 𝜑 → ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) = ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) ) |
40 |
|
ssid |
⊢ 𝑁 ⊆ 𝑁 |
41 |
|
resmpo |
⊢ ( ( { 𝐼 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ) |
42 |
25 40 41
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ) |
43 |
|
resmpo |
⊢ ( ( { 𝐼 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) |
44 |
25 40 43
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) |
45 |
|
resmpo |
⊢ ( ( { 𝐼 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) |
46 |
25 40 45
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) |
47 |
44 46
|
oveq12d |
⊢ ( 𝜑 → ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ) = ( ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ∘f + ( 𝑖 ∈ { 𝐼 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) ) |
48 |
39 42 47
|
3eqtr4d |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ∘f + ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ) ) |
49 |
|
eldifsni |
⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑖 ≠ 𝐼 ) |
50 |
49
|
neneqd |
⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → ¬ 𝑖 = 𝐼 ) |
51 |
|
iffalse |
⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = 𝑍 ) |
52 |
|
iffalse |
⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) = 𝑍 ) |
53 |
51 52
|
eqtr4d |
⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) |
54 |
50 53
|
syl |
⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) |
55 |
54
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) |
56 |
55
|
mpoeq3dva |
⊢ ( 𝜑 → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) |
57 |
|
difss |
⊢ ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 |
58 |
|
resmpo |
⊢ ( ( ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ) |
59 |
57 40 58
|
mp2an |
⊢ ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) |
60 |
|
resmpo |
⊢ ( ( ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) |
61 |
57 40 60
|
mp2an |
⊢ ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) |
62 |
56 59 61
|
3eqtr4g |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ) |
63 |
|
iffalse |
⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) = 𝑍 ) |
64 |
51 63
|
eqtr4d |
⊢ ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) |
65 |
50 64
|
syl |
⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) |
66 |
65
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) = if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) |
67 |
66
|
mpoeq3dva |
⊢ ( 𝜑 → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) |
68 |
|
resmpo |
⊢ ( ( ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) |
69 |
57 40 68
|
mp2an |
⊢ ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) |
70 |
67 59 69
|
3eqtr4g |
⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) ) |
71 |
1 10 11 3 4 18 20 22 9 48 62 70
|
mdetrlin |
⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) ) ) |