This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdetrlin2

Description: The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mdetrlin2.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetrlin2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetrlin2.p ⊢ + = ( +g ‘ 𝑅 )
mdetrlin2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetrlin2.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetrlin2.x ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
mdetrlin2.y ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐾 )
mdetrlin2.z ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑍 ∈ 𝐾 )
mdetrlin2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
Assertion mdetrlin2 ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝑋 + 𝑌 ) , 𝑍 ) ) ) = ( ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑍 ) ) ) + ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) ) )

Proof

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 ( 𝑖 = 𝐼 , 𝑌 , 𝑍 ) ) ) ) )