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