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