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 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( { 𝐾 } × 𝑁 ) ) ) )