Metamath Proof Explorer


Theorem mdetrsca2

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

Ref Expression
Hypotheses mdetrsca2.d 𝐷 = ( 𝑁 maDet 𝑅 )
mdetrsca2.k 𝐾 = ( Base ‘ 𝑅 )
mdetrsca2.t · = ( .r𝑅 )
mdetrsca2.r ( 𝜑𝑅 ∈ CRing )
mdetrsca2.n ( 𝜑𝑁 ∈ Fin )
mdetrsca2.x ( ( 𝜑𝑖𝑁𝑗𝑁 ) → 𝑋𝐾 )
mdetrsca2.y ( ( 𝜑𝑖𝑁𝑗𝑁 ) → 𝑌𝐾 )
mdetrsca2.f ( 𝜑𝐹𝐾 )
mdetrsca2.i ( 𝜑𝐼𝑁 )
Assertion mdetrsca2 ( 𝜑 → ( 𝐷 ‘ ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ) = ( 𝐹 · ( 𝐷 ‘ ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mdetrsca2.d 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetrsca2.k 𝐾 = ( Base ‘ 𝑅 )
3 mdetrsca2.t · = ( .r𝑅 )
4 mdetrsca2.r ( 𝜑𝑅 ∈ CRing )
5 mdetrsca2.n ( 𝜑𝑁 ∈ Fin )
6 mdetrsca2.x ( ( 𝜑𝑖𝑁𝑗𝑁 ) → 𝑋𝐾 )
7 mdetrsca2.y ( ( 𝜑𝑖𝑁𝑗𝑁 ) → 𝑌𝐾 )
8 mdetrsca2.f ( 𝜑𝐹𝐾 )
9 mdetrsca2.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 8 3ad2ant1 ( ( 𝜑𝑖𝑁𝑗𝑁 ) → 𝐹𝐾 )
16 2 3 ringcl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐾𝑋𝐾 ) → ( 𝐹 · 𝑋 ) ∈ 𝐾 )
17 14 15 6 16 syl3anc ( ( 𝜑𝑖𝑁𝑗𝑁 ) → ( 𝐹 · 𝑋 ) ∈ 𝐾 )
18 17 7 ifcld ( ( 𝜑𝑖𝑁𝑗𝑁 ) → if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ∈ 𝐾 )
19 10 2 11 5 4 18 matbas2d ( 𝜑 → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
20 6 7 ifcld ( ( 𝜑𝑖𝑁𝑗𝑁 ) → if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ∈ 𝐾 )
21 10 2 11 5 4 20 matbas2d ( 𝜑 → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
22 snex { 𝐼 } ∈ V
23 22 a1i ( 𝜑 → { 𝐼 } ∈ V )
24 8 3ad2ant1 ( ( 𝜑𝑖 ∈ { 𝐼 } ∧ 𝑗𝑁 ) → 𝐹𝐾 )
25 9 snssd ( 𝜑 → { 𝐼 } ⊆ 𝑁 )
26 25 sselda ( ( 𝜑𝑖 ∈ { 𝐼 } ) → 𝑖𝑁 )
27 26 3adant3 ( ( 𝜑𝑖 ∈ { 𝐼 } ∧ 𝑗𝑁 ) → 𝑖𝑁 )
28 27 6 syld3an2 ( ( 𝜑𝑖 ∈ { 𝐼 } ∧ 𝑗𝑁 ) → 𝑋𝐾 )
29 fconstmpo ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝐹 )
30 29 a1i ( 𝜑 → ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝐹 ) )
31 eqidd ( 𝜑 → ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝑋 ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝑋 ) )
32 23 5 24 28 30 31 offval22 ( 𝜑 → ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝑋 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ ( 𝐹 · 𝑋 ) ) )
33 mposnif ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝑋 )
34 33 oveq2i ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ) = ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁𝑋 ) )
35 mposnif ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ ( 𝐹 · 𝑋 ) )
36 32 34 35 3eqtr4g ( 𝜑 → ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) )
37 ssid 𝑁𝑁
38 resmpo ( ( { 𝐼 } ⊆ 𝑁𝑁𝑁 ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) )
39 25 37 38 sylancl ( 𝜑 → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) )
40 39 oveq2d ( 𝜑 → ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ) = ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ) )
41 resmpo ( ( { 𝐼 } ⊆ 𝑁𝑁𝑁 ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) )
42 25 37 41 sylancl ( 𝜑 → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐼 } , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) )
43 36 40 42 3eqtr4rd ( 𝜑 → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) = ( ( ( { 𝐼 } × 𝑁 ) × { 𝐹 } ) ∘f · ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( { 𝐼 } × 𝑁 ) ) ) )
44 eldifsni ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑖𝐼 )
45 44 3ad2ant2 ( ( 𝜑𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗𝑁 ) → 𝑖𝐼 )
46 45 neneqd ( ( 𝜑𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗𝑁 ) → ¬ 𝑖 = 𝐼 )
47 iffalse ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) = 𝑌 )
48 iffalse ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) = 𝑌 )
49 47 48 eqtr4d ( ¬ 𝑖 = 𝐼 → if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) )
50 46 49 syl ( ( 𝜑𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) ∧ 𝑗𝑁 ) → if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) = if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) )
51 50 mpoeq3dva ( 𝜑 → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) )
52 difss ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁
53 resmpo ( ( ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁𝑁𝑁 ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) )
54 52 37 53 mp2an ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) )
55 resmpo ( ( ( 𝑁 ∖ { 𝐼 } ) ⊆ 𝑁𝑁𝑁 ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) )
56 52 37 55 mp2an ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐼 } ) , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) )
57 51 54 56 3eqtr4g ( 𝜑 → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) = ( ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ↾ ( ( 𝑁 ∖ { 𝐼 } ) × 𝑁 ) ) )
58 1 10 11 2 3 4 19 8 21 9 43 57 mdetrsca ( 𝜑 → ( 𝐷 ‘ ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , ( 𝐹 · 𝑋 ) , 𝑌 ) ) ) = ( 𝐹 · ( 𝐷 ‘ ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐼 , 𝑋 , 𝑌 ) ) ) ) )