Metamath Proof Explorer

Theorem smadiadetglem2

Description: Lemma 2 for smadiadetg . (Contributed by AV, 14-Feb-2019)

Ref Expression
Hypotheses smadiadet.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
smadiadet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
smadiadet.r ⊢ 𝑅 ∈ CRing
smadiadet.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
smadiadet.h ⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
smadiadetg.x ⊢ · = ( .r ‘ 𝑅 )
Assertion smadiadetglem2 ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 smadiadet.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 smadiadet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 smadiadet.r ⊢ 𝑅 ∈ CRing
4 smadiadet.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
5 smadiadet.h ⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
6 smadiadetg.x ⊢ · = ( .r ‘ 𝑅 )
7 snex ⊢ { 𝐾 } ∈ V
8 7 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → { 𝐾 } ∈ V )
9 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10 elex ⊢ ( 𝑁 ∈ Fin → 𝑁 ∈ V )
11 10 adantr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝑁 ∈ V )
12 9 11 syl ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ V )
13 12 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑁 ∈ V )
14 simp13 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 ∈ { 𝐾 } ∧ 𝑗 ∈ 𝑁 ) → 𝑆 ∈ ( Base ‘ 𝑅 ) )
15 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16 3 15 mp1i ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 ∈ { 𝐾 } ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
17 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19 17 18 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
20 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
21 17 20 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
22 19 21 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
23 16 22 syl ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 ∈ { 𝐾 } ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
24 fconstmpo ⊢ ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ 𝑆 )
25 24 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ 𝑆 ) )
26 eqidd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
27 8 13 14 23 25 26 offval22 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
28 3 15 mp1i ⊢ ( 𝑆 ∈ ( Base ‘ 𝑅 ) → 𝑅 ∈ Ring )
29 17 6 18 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 · ( 1r ‘ 𝑅 ) ) = 𝑆 )
30 28 29 mpancom ⊢ ( 𝑆 ∈ ( Base ‘ 𝑅 ) → ( 𝑆 · ( 1r ‘ 𝑅 ) ) = 𝑆 )
31 30 3ad2ant3 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 · ( 1r ‘ 𝑅 ) ) = 𝑆 )
32 31 ad2antrl ⊢ ( ( 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · ( 1r ‘ 𝑅 ) ) = 𝑆 )
33 iftrue ⊢ ( 𝑗 = 𝐾 → if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
34 33 adantr ⊢ ( ( 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
35 34 oveq2d ⊢ ( ( 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑆 · ( 1r ‘ 𝑅 ) ) )
36 iftrue ⊢ ( 𝑗 = 𝐾 → if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) = 𝑆 )
37 36 adantr ⊢ ( ( 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) = 𝑆 )
38 32 35 37 3eqtr4d ⊢ ( ( 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) )
39 17 6 20 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
40 28 39 mpancom ⊢ ( 𝑆 ∈ ( Base ‘ 𝑅 ) → ( 𝑆 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
41 40 3ad2ant3 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
42 41 ad2antrl ⊢ ( ( ¬ 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
43 iffalse ⊢ ( ¬ 𝑗 = 𝐾 → if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
44 43 oveq2d ⊢ ( ¬ 𝑗 = 𝐾 → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑆 · ( 0g ‘ 𝑅 ) ) )
45 44 adantr ⊢ ( ( ¬ 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑆 · ( 0g ‘ 𝑅 ) ) )
46 iffalse ⊢ ( ¬ 𝑗 = 𝐾 → if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
47 46 adantr ⊢ ( ( ¬ 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
48 42 45 47 3eqtr4d ⊢ ( ( ¬ 𝑗 = 𝐾 ∧ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) )
49 38 48 pm2.61ian ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) )
50 49 3adant2 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 ∈ { 𝐾 } ∧ 𝑗 ∈ 𝑁 ) → ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) )
51 50 mpoeq3dva ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ ( 𝑆 · if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) ) )
52 27 51 eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) ) )
53 simp2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝐾 ∈ 𝑁 )
54 eqid ⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑁 minMatR1 𝑅 )
55 1 2 54 18 20 minmar1val ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
56 53 55 syld3an3 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
57 56 reseq1d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) )
58 snssi ⊢ ( 𝐾 ∈ 𝑁 → { 𝐾 } ⊆ 𝑁 )
59 58 3ad2ant2 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → { 𝐾 } ⊆ 𝑁 )
60 ssid ⊢ 𝑁 ⊆ 𝑁
61 resmpo ⊢ ( ( { 𝐾 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
62 59 60 61 sylancl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
63 mposnif ⊢ ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
64 63 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
65 57 62 64 3eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
66 65 oveq2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) ) = ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
67 3simpb ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) )
68 eqid ⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
69 1 2 68 20 marrepval ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
70 67 53 53 69 syl12anc ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
71 70 reseq1d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) )
72 resmpo ⊢ ( ( { 𝐾 } ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
73 59 60 72 sylancl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
74 mposnif ⊢ ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) )
75 74 a1i ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) ) )
76 71 73 75 3eqtrd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( 𝑖 ∈ { 𝐾 } , 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) ) )
77 52 66 76 3eqtr4rd ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) = ( ( ( { 𝐾 } × 𝑁 ) × { 𝑆 } ) ∘f · ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) ) )