Metamath Proof Explorer

Theorem madjusmdetlem1

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madjusmdet.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
madjusmdet.d ⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
madjusmdet.k ⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
madjusmdet.t ⊢ · = ( .r ‘ 𝑅 )
madjusmdet.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
madjusmdet.e ⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
madjusmdet.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
madjusmdet.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
madjusmdet.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
madjusmdet.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
madjusmdet.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
madjusmdetlem1.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
madjusmdetlem1.s ⊢ 𝑆 = ( pmSgn ‘ ( 1 ... 𝑁 ) )
madjusmdetlem1.u ⊢ 𝑈 = ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 )
madjusmdetlem1.w ⊢ 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) )
madjusmdetlem1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐺 )
madjusmdetlem1.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐺 )
madjusmdetlem1.1 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = 𝐼 )
madjusmdetlem1.2 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = 𝐽 )
madjusmdetlem1.3 ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) )
Assertion madjusmdetlem1 ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 madjusmdet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
2 madjusmdet.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
3 madjusmdet.d ⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
4 madjusmdet.k ⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
5 madjusmdet.t ⊢ · = ( .r ‘ 𝑅 )
6 madjusmdet.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
7 madjusmdet.e ⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
8 madjusmdet.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 madjusmdet.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
10 madjusmdet.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
11 madjusmdet.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
12 madjusmdet.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
13 madjusmdetlem1.g ⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )
14 madjusmdetlem1.s ⊢ 𝑆 = ( pmSgn ‘ ( 1 ... 𝑁 ) )
15 madjusmdetlem1.u ⊢ 𝑈 = ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 )
16 madjusmdetlem1.w ⊢ 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) )
17 madjusmdetlem1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐺 )
18 madjusmdetlem1.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐺 )
19 madjusmdetlem1.1 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = 𝐼 )
20 madjusmdetlem1.2 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = 𝐽 )
21 madjusmdetlem1.3 ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) = ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) )
22 2 1 3 4 maducoevalmin1 ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( 𝐷 ‘ ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ) )
23 12 11 10 22 syl3anc ⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( 𝐷 ‘ ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ) )
24 15 fveq2i ⊢ ( 𝐷 ‘ 𝑈 ) = ( 𝐷 ‘ ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) )
25 23 24 eqtr4di ⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( 𝐷 ‘ 𝑈 ) )
26 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
27 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
28 9 27 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
29 2 1 minmar1cl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ∈ 𝐵 )
30 28 12 10 11 29 syl22anc ⊢ ( 𝜑 → ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ∈ 𝐵 )
31 15 30 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
32 2 1 3 13 14 6 5 16 9 26 31 17 18 mdetpmtr12 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑈 ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝑊 ) ) )
33 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → 𝑖 = 𝑁 )
34 33 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑁 ) )
35 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑁 ) = 𝐼 )
36 35 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑁 ) = 𝐼 )
37 34 36 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑖 ) = 𝐼 )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → 𝑗 = 𝑁 )
39 38 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑁 ) )
40 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑁 ) = 𝐽 )
41 40 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑄 ‘ 𝑁 ) = 𝐽 )
42 39 41 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝑄 ‘ 𝑗 ) = 𝐽 )
43 37 42 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) = ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) 𝐽 ) )
44 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ 𝐵 )
45 44 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → 𝑀 ∈ 𝐵 )
46 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
47 46 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
48 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐽 ∈ ( 1 ... 𝑁 ) )
49 48 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → 𝐽 ∈ ( 1 ... 𝑁 ) )
50 eqid ⊢ ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) = ( ( 1 ... 𝑁 ) minMatR1 𝑅 )
51 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
52 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
53 2 1 50 51 52 minmar1eval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) 𝐽 ) = if ( 𝐼 = 𝐼 , if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 𝐽 ) ) )
54 45 47 49 47 49 53 syl122anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) 𝐽 ) = if ( 𝐼 = 𝐼 , if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 𝐽 ) ) )
55 eqid ⊢ 𝐼 = 𝐼
56 55 iftruei ⊢ if ( 𝐼 = 𝐼 , if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 𝐽 ) ) = if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) )
57 eqid ⊢ 𝐽 = 𝐽
58 57 iftruei ⊢ if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 )
59 56 58 eqtri ⊢ if ( 𝐼 = 𝐼 , if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 𝐽 ) ) = ( 1r ‘ 𝑅 )
60 59 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → if ( 𝐼 = 𝐼 , if ( 𝐽 = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 𝐽 ) ) = ( 1r ‘ 𝑅 ) )
61 43 54 60 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ 𝑗 = 𝑁 ) → ( 1r ‘ 𝑅 ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
62 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → 𝑖 = 𝑁 )
63 62 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑁 ) )
64 35 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑁 ) = 𝐼 )
65 63 64 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 𝑃 ‘ 𝑖 ) = 𝐼 )
66 65 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) = ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
67 44 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → 𝑀 ∈ 𝐵 )
68 46 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → 𝐼 ∈ ( 1 ... 𝑁 ) )
69 48 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → 𝐽 ∈ ( 1 ... 𝑁 ) )
70 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑄 ∈ 𝐺 )
71 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
72 eqid ⊢ ( SymGrp ‘ ( 1 ... 𝑁 ) ) = ( SymGrp ‘ ( 1 ... 𝑁 ) )
73 72 13 symgfv ⊢ ( ( 𝑄 ∈ 𝐺 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
74 70 71 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
75 74 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 𝑄 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) )
76 2 1 50 51 52 minmar1eval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ 𝐽 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐼 ∈ ( 1 ... 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) ∈ ( 1 ... 𝑁 ) ) ) → ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) = if ( 𝐼 = 𝐼 , if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) )
77 67 68 69 68 75 76 syl122anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 𝐼 ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) = if ( 𝐼 = 𝐼 , if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) )
78 55 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → 𝐼 = 𝐼 )
79 78 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → if ( 𝐼 = 𝐼 , if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) = if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
80 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → ( 𝑄 ‘ 𝑗 ) = 𝐽 )
81 80 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑗 ) ) = ( ◡ 𝑄 ‘ 𝐽 ) )
82 72 13 symgbasf1o ⊢ ( 𝑄 ∈ 𝐺 → 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
83 70 82 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
84 83 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
85 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
86 f1ocnvfv1 ⊢ ( ( 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑗 ) ) = 𝑗 )
87 84 85 86 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑗 ) ) = 𝑗 )
88 20 fveq2d ⊢ ( 𝜑 → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑁 ) ) = ( ◡ 𝑄 ‘ 𝐽 ) )
89 18 82 syl ⊢ ( 𝜑 → 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
90 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
91 8 90 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
92 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
93 91 92 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
94 f1ocnvfv1 ⊢ ( ( 𝑄 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑁 ) ) = 𝑁 )
95 89 93 94 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑄 ‘ ( 𝑄 ‘ 𝑁 ) ) = 𝑁 )
96 88 95 eqtr3d ⊢ ( 𝜑 → ( ◡ 𝑄 ‘ 𝐽 ) = 𝑁 )
97 96 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ◡ 𝑄 ‘ 𝐽 ) = 𝑁 )
98 97 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → ( ◡ 𝑄 ‘ 𝐽 ) = 𝑁 )
99 81 87 98 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) → 𝑗 = 𝑁 )
100 99 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) → ( ( 𝑄 ‘ 𝑗 ) = 𝐽 → 𝑗 = 𝑁 ) )
101 100 con3d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) → ( ¬ 𝑗 = 𝑁 → ¬ ( 𝑄 ‘ 𝑗 ) = 𝐽 ) )
102 101 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ¬ ( 𝑄 ‘ 𝑗 ) = 𝐽 )
103 102 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
104 79 103 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → if ( 𝐼 = 𝐼 , if ( ( 𝑄 ‘ 𝑗 ) = 𝐽 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝐼 𝑀 ( 𝑄 ‘ 𝑗 ) ) ) = ( 0g ‘ 𝑅 ) )
105 66 77 104 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) ∧ ¬ 𝑗 = 𝑁 ) → ( 0g ‘ 𝑅 ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
106 61 105 ifeqda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑖 = 𝑁 ) → if ( 𝑗 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
107 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑖 = 𝑁 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
109 71 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑖 = 𝑁 ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
110 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑖 = 𝑁 ) → ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) ∈ V )
111 15 oveqi ⊢ ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) )
112 111 a1i ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
113 112 mpoeq3ia ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
114 16 113 eqtri ⊢ 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
115 114 ovmpt4g ⊢ ( ( 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ∧ ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) ∈ V ) → ( 𝑖 𝑊 𝑗 ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
116 108 109 110 115 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑖 = 𝑁 ) → ( 𝑖 𝑊 𝑗 ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
117 106 116 ifeqda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑖 = 𝑁 , if ( 𝑗 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑊 𝑗 ) ) = ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) )
118 117 mpoeq3dva ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 𝑁 , if ( 𝑗 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑊 𝑗 ) ) ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) ) )
119 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
120 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑃 ∈ 𝐺 )
121 72 13 symgfv ⊢ ( ( 𝑃 ∈ 𝐺 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ( 1 ... 𝑁 ) )
122 120 107 121 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ( 1 ... 𝑁 ) )
123 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ 𝐵 )
124 2 119 1 122 74 123 matecld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
125 2 119 1 26 9 124 matbas2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) 𝑈 ( 𝑄 ‘ 𝑗 ) ) ) ∈ 𝐵 )
126 16 125 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
127 119 51 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
128 28 127 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
129 eqid ⊢ ( ( 1 ... 𝑁 ) matRRep 𝑅 ) = ( ( 1 ... 𝑁 ) matRRep 𝑅 )
130 2 1 129 52 marrepval ⊢ ( ( ( 𝑊 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑁 ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) ) → ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 𝑁 , if ( 𝑗 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑊 𝑗 ) ) ) )
131 126 128 93 93 130 syl22anc ⊢ ( 𝜑 → ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 𝑁 , if ( 𝑗 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑊 𝑗 ) ) ) )
132 114 a1i ⊢ ( 𝜑 → 𝑊 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑃 ‘ 𝑖 ) ( 𝐼 ( ( ( 1 ... 𝑁 ) minMatR1 𝑅 ) ‘ 𝑀 ) 𝐽 ) ( 𝑄 ‘ 𝑗 ) ) ) )
133 118 131 132 3eqtr4d ⊢ ( 𝜑 → ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) = 𝑊 )
134 133 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( 𝐷 ‘ 𝑊 ) )
135 eqid ⊢ ( ( 1 ... 𝑁 ) subMat 𝑅 ) = ( ( 1 ... 𝑁 ) subMat 𝑅 )
136 2 135 1 submaval ⊢ ( ( 𝑊 ∈ 𝐵 ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑊 𝑗 ) ) )
137 126 93 93 136 syl3anc ⊢ ( 𝜑 → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑊 𝑗 ) ) )
138 fzdif2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
139 91 138 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
140 mpoeq12 ⊢ ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) ∧ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑊 𝑗 ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑊 𝑗 ) ) )
141 139 139 140 syl2anc ⊢ ( 𝜑 → ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑊 𝑗 ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑊 𝑗 ) ) )
142 137 141 eqtrd ⊢ ( 𝜑 → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑊 𝑗 ) ) )
143 difssd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ⊆ ( 1 ... 𝑁 ) )
144 139 143 eqsstrrd ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
145 2 1 submabas ⊢ ( ( 𝑊 ∈ 𝐵 ∧ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) ) → ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑊 𝑗 ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
146 126 144 145 syl2anc ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑊 𝑗 ) ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
147 142 146 eqeltrd ⊢ ( 𝜑 → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
148 eqid ⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
149 eqid ⊢ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
150 7 148 149 119 mdetcl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) → ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ∈ ( Base ‘ 𝑅 ) )
151 9 147 150 syl2anc ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ∈ ( Base ‘ 𝑅 ) )
152 119 5 51 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) · ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) = ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) )
153 28 151 152 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) = ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) )
154 2 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) )
155 1 154 eqtri ⊢ 𝐵 = ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) )
156 126 155 eleqtrdi ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) )
157 smadiadetr ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑊 ∈ ( Base ‘ ( ( 1 ... 𝑁 ) Mat 𝑅 ) ) ) ∧ ( 𝑁 ∈ ( 1 ... 𝑁 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( 1 ... 𝑁 ) maDet 𝑅 ) ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
158 9 156 93 128 157 syl22anc ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) maDet 𝑅 ) ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
159 3 fveq1i ⊢ ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( ( 1 ... 𝑁 ) maDet 𝑅 ) ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) )
160 5 oveqi ⊢ ( ( 1r ‘ 𝑅 ) · ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) )
161 159 160 eqeq12i ⊢ ( ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) ↔ ( ( ( 1 ... 𝑁 ) maDet 𝑅 ) ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
162 158 161 sylibr ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) · ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
163 139 oveq1d ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 ) )
164 163 7 eqtr4di ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) = 𝐸 )
165 164 fveq1d ⊢ ( 𝜑 → ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) = ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) )
166 165 oveq2d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) maDet 𝑅 ) ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
167 162 166 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( ( 1r ‘ 𝑅 ) · ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) ) )
168 2 1 submat1n ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑊 ∈ 𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) = ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) )
169 8 126 168 syl2anc ⊢ ( 𝜑 → ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) = ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) )
170 169 fveq2d ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) ) = ( 𝐸 ‘ ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑊 ) 𝑁 ) ) )
171 153 167 170 3eqtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ( 𝑊 ( ( 1 ... 𝑁 ) matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝑁 ) ) = ( 𝐸 ‘ ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) ) )
172 134 171 eqtr3d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) ) )
173 2 1 8 10 11 28 12 15 submatminr1 ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) = ( 𝐼 ( subMat1 ‘ 𝑈 ) 𝐽 ) )
174 173 21 eqtrd ⊢ ( 𝜑 → ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) = ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) )
175 174 fveq2d ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) = ( 𝐸 ‘ ( 𝑁 ( subMat1 ‘ 𝑊 ) 𝑁 ) ) )
176 172 175 eqtr4d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) )
177 176 oveq2d ⊢ ( 𝜑 → ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐷 ‘ 𝑊 ) ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )
178 25 32 177 3eqtrd ⊢ ( 𝜑 → ( 𝐽 ( 𝐾 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑍 ‘ ( ( 𝑆 ‘ 𝑃 ) · ( 𝑆 ‘ 𝑄 ) ) ) · ( 𝐸 ‘ ( 𝐼 ( subMat1 ‘ 𝑀 ) 𝐽 ) ) ) )