Theorem smadiadetglem1

Description: Lemma 1 for smadiadetg . (Contributed by AV, 13-Feb-2019)

	Ref	Expression
Hypotheses	smadiadet.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	smadiadet.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	smadiadet.r	⊢ 𝑅 ∈ CRing
	smadiadet.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	smadiadet.h	⊢ 𝐸 = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
Assertion	smadiadetglem1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝐾 ( ( 𝑁 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		mpodifsnif	⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) )
7		mpodifsnif	⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ ( 𝑖 𝑀 𝑗 ) )
8	6 7	eqtr4i	⊢ ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) )
9		difss	⊢ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁
10		ssid	⊢ 𝑁 ⊆ 𝑁
11	9 10	pm3.2i	⊢ ( ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 )
12		resmpo	⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
13	11 12	mp1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
14		resmpo	⊢ ( ( ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ∧ 𝑁 ⊆ 𝑁 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
15	11 14	mp1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
16	8 13 15	3eqtr4a	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
17		simp1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑀 ∈ 𝐵 )
18		simp3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝑆 ∈ ( Base ‘ 𝑅 ) )
19		simp2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → 𝐾 ∈ 𝑁 )
20		eqid	⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
21		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
22	1 2 20 21	marrepval	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
23	17 18 19 19 22	syl22anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
24	23	reseq1d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , 𝑆 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
25		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
28	26 27	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29	25 28	syl	⊢ ( 𝑅 ∈ CRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
30	3 29	mp1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
31	1 2 20 21	marrepval	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
32	17 30 19 19 31	syl22anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) )
33	32	reseq1d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐾 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
34	16 24 33	3eqtr4d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
35	3 25	ax-mp	⊢ 𝑅 ∈ Ring
36	1 2 27	minmar1marrep	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
37	35 17 36	sylancr	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
38	37	eqcomd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) )
39	38	oveqd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) = ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) )
40	39	reseq1d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )
41	34 40	eqtrd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) = ( ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐾 ) ↾ ( ( 𝑁 ∖ { 𝐾 } ) × 𝑁 ) ) )