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