Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  madjusmdetlem1 Structured version   Visualization version   GIF version

 Description: Lemma for madjusmdet 31098. (Contributed by Thierry Arnoux, 22-Aug-2020.)
Hypotheses
Ref Expression
madjusmdet.a 𝐴 = ((1...𝑁) Mat 𝑅)
madjusmdetlem1.u 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
madjusmdetlem1.w 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)𝑈(𝑄𝑗)))
madjusmdetlem1.1 (𝜑 → (𝑃𝑁) = 𝐼)
madjusmdetlem1.2 (𝜑 → (𝑄𝑁) = 𝐽)
madjusmdetlem1.3 (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
Assertion
Ref Expression
madjusmdetlem1 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘((𝑆𝑃) · (𝑆𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
Distinct variable groups:   𝐵,𝑖,𝑗   𝑖,𝐼,𝑗   𝑖,𝐽,𝑗   𝑖,𝑀,𝑗   𝑖,𝑁,𝑗   𝑃,𝑖,𝑗   𝑄,𝑖,𝑗   𝑅,𝑖,𝑗   𝜑,𝑖,𝑗   𝑖,𝐺,𝑗   𝑖,𝑊,𝑗   𝑈,𝑖,𝑗
Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖,𝑗)   𝑆(𝑖,𝑗)   · (𝑖,𝑗)   𝐸(𝑖,𝑗)   𝐾(𝑖,𝑗)   𝑍(𝑖,𝑗)

StepHypRef Expression
1 madjusmdet.m . . . 4 (𝜑𝑀𝐵)
2 madjusmdet.j . . . 4 (𝜑𝐽 ∈ (1...𝑁))
3 madjusmdet.i . . . 4 (𝜑𝐼 ∈ (1...𝑁))
4 madjusmdet.a . . . . 5 𝐴 = ((1...𝑁) Mat 𝑅)
5 madjusmdet.b . . . . 5 𝐵 = (Base‘𝐴)
6 madjusmdet.d . . . . 5 𝐷 = ((1...𝑁) maDet 𝑅)
7 madjusmdet.k . . . . 5 𝐾 = ((1...𝑁) maAdju 𝑅)
84, 5, 6, 7maducoevalmin1 21263 . . . 4 ((𝑀𝐵𝐽 ∈ (1...𝑁) ∧ 𝐼 ∈ (1...𝑁)) → (𝐽(𝐾𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
91, 2, 3, 8syl3anc 1367 . . 3 (𝜑 → (𝐽(𝐾𝑀)𝐼) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)))
10 madjusmdetlem1.u . . . 4 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)
1110fveq2i 6675 . . 3 (𝐷𝑈) = (𝐷‘(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽))
129, 11syl6eqr 2876 . 2 (𝜑 → (𝐽(𝐾𝑀)𝐼) = (𝐷𝑈))
13 madjusmdetlem1.g . . 3 𝐺 = (Base‘(SymGrp‘(1...𝑁)))
14 madjusmdetlem1.s . . 3 𝑆 = (pmSgn‘(1...𝑁))
15 madjusmdet.z . . 3 𝑍 = (ℤRHom‘𝑅)
16 madjusmdet.t . . 3 · = (.r𝑅)
17 madjusmdetlem1.w . . 3 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)𝑈(𝑄𝑗)))
18 madjusmdet.r . . 3 (𝜑𝑅 ∈ CRing)
19 fzfid 13344 . . 3 (𝜑 → (1...𝑁) ∈ Fin)
20 crngring 19310 . . . . . 6 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
2118, 20syl 17 . . . . 5 (𝜑𝑅 ∈ Ring)
224, 5minmar1cl 21262 . . . . 5 (((𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
2321, 1, 3, 2, 22syl22anc 836 . . . 4 (𝜑 → (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ∈ 𝐵)
2410, 23eqeltrid 2919 . . 3 (𝜑𝑈𝐵)
25 madjusmdetlem1.p . . 3 (𝜑𝑃𝐺)
26 madjusmdetlem1.q . . 3 (𝜑𝑄𝐺)
274, 5, 6, 13, 14, 15, 16, 17, 18, 19, 24, 25, 26mdetpmtr12 31092 . 2 (𝜑 → (𝐷𝑈) = ((𝑍‘((𝑆𝑃) · (𝑆𝑄))) · (𝐷𝑊)))
28 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑖 = 𝑁)
2928fveq2d 6676 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃𝑖) = (𝑃𝑁))
30 madjusmdetlem1.1 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃𝑁) = 𝐼)
31303ad2ant1 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃𝑁) = 𝐼)
3231ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃𝑁) = 𝐼)
3329, 32eqtrd 2858 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑃𝑖) = 𝐼)
34 simpr 487 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑗 = 𝑁)
3534fveq2d 6676 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄𝑗) = (𝑄𝑁))
36 madjusmdetlem1.2 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄𝑁) = 𝐽)
37363ad2ant1 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄𝑁) = 𝐽)
3837ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄𝑁) = 𝐽)
3935, 38eqtrd 2858 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝑄𝑗) = 𝐽)
4033, 39oveq12d 7176 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽))
4113ad2ant1 1129 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑀𝐵)
4241ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝑀𝐵)
4333ad2ant1 1129 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐼 ∈ (1...𝑁))
4443ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
4523ad2ant1 1129 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝐽 ∈ (1...𝑁))
4645ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
47 eqid 2823 . . . . . . . . . . . . 13 ((1...𝑁) minMatR1 𝑅) = ((1...𝑁) minMatR1 𝑅)
48 eqid 2823 . . . . . . . . . . . . 13 (1r𝑅) = (1r𝑅)
49 eqid 2823 . . . . . . . . . . . . 13 (0g𝑅) = (0g𝑅)
504, 5, 47, 48, 49minmar1eval 21260 . . . . . . . . . . . 12 ((𝑀𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀𝐽)))
5142, 44, 46, 44, 46, 50syl122anc 1375 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)𝐽) = if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀𝐽)))
52 eqid 2823 . . . . . . . . . . . . . 14 𝐼 = 𝐼
5352iftruei 4476 . . . . . . . . . . . . 13 if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀𝐽)) = if(𝐽 = 𝐽, (1r𝑅), (0g𝑅))
54 eqid 2823 . . . . . . . . . . . . . 14 𝐽 = 𝐽
5554iftruei 4476 . . . . . . . . . . . . 13 if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)) = (1r𝑅)
5653, 55eqtri 2846 . . . . . . . . . . . 12 if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀𝐽)) = (1r𝑅)
5756a1i 11 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if(𝐽 = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀𝐽)) = (1r𝑅))
5840, 51, 573eqtrrd 2863 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ 𝑗 = 𝑁) → (1r𝑅) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
59 simplr 767 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑖 = 𝑁)
6059fveq2d 6676 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃𝑖) = (𝑃𝑁))
6131ad2antrr 724 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃𝑁) = 𝐼)
6260, 61eqtrd 2858 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑃𝑖) = 𝐼)
6362oveq1d 7173 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) = (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
6441ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝑀𝐵)
6543ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 ∈ (1...𝑁))
6645ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐽 ∈ (1...𝑁))
67263ad2ant1 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄𝐺)
68 simp3 1134 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
69 eqid 2823 . . . . . . . . . . . . . . 15 (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
7069, 13symgfv 18510 . . . . . . . . . . . . . 14 ((𝑄𝐺𝑗 ∈ (1...𝑁)) → (𝑄𝑗) ∈ (1...𝑁))
7167, 68, 70syl2anc 586 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄𝑗) ∈ (1...𝑁))
7271ad2antrr 724 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝑄𝑗) ∈ (1...𝑁))
734, 5, 47, 48, 49minmar1eval 21260 . . . . . . . . . . . 12 ((𝑀𝐵 ∧ (𝐼 ∈ (1...𝑁) ∧ 𝐽 ∈ (1...𝑁)) ∧ (𝐼 ∈ (1...𝑁) ∧ (𝑄𝑗) ∈ (1...𝑁))) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) = if(𝐼 = 𝐼, if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀(𝑄𝑗))))
7464, 65, 66, 65, 72, 73syl122anc 1375 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (𝐼(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) = if(𝐼 = 𝐼, if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀(𝑄𝑗))))
7552a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → 𝐼 = 𝐼)
7675iftrued 4477 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀(𝑄𝑗))) = if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)))
77 simpr 487 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → (𝑄𝑗) = 𝐽)
7877fveq2d 6676 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → (𝑄‘(𝑄𝑗)) = (𝑄𝐽))
7969, 13symgbasf1o 18505 . . . . . . . . . . . . . . . . . . . 20 (𝑄𝐺𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
8067, 79syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
8180ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → 𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
8268ad2antrr 724 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → 𝑗 ∈ (1...𝑁))
83 f1ocnvfv1 7035 . . . . . . . . . . . . . . . . . 18 ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄‘(𝑄𝑗)) = 𝑗)
8481, 82, 83syl2anc 586 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → (𝑄‘(𝑄𝑗)) = 𝑗)
8536fveq2d 6676 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑄‘(𝑄𝑁)) = (𝑄𝐽))
8626, 79syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑄:(1...𝑁)–1-1-onto→(1...𝑁))
87 madjusmdet.n . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑁 ∈ ℕ)
88 nnuz 12284 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
8987, 88eleqtrdi 2925 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑁 ∈ (ℤ‘1))
90 eluzfz2 12918 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ (1...𝑁))
92 f1ocnvfv1 7035 . . . . . . . . . . . . . . . . . . . . 21 ((𝑄:(1...𝑁)–1-1-onto→(1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑄‘(𝑄𝑁)) = 𝑁)
9386, 91, 92syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑄‘(𝑄𝑁)) = 𝑁)
9485, 93eqtr3d 2860 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄𝐽) = 𝑁)
95943ad2ant1 1129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑄𝐽) = 𝑁)
9695ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → (𝑄𝐽) = 𝑁)
9778, 84, 963eqtr3d 2866 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ (𝑄𝑗) = 𝐽) → 𝑗 = 𝑁)
9897ex 415 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → ((𝑄𝑗) = 𝐽𝑗 = 𝑁))
9998con3d 155 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → (¬ 𝑗 = 𝑁 → ¬ (𝑄𝑗) = 𝐽))
10099imp 409 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → ¬ (𝑄𝑗) = 𝐽)
101100iffalsed 4480 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)) = (0g𝑅))
10276, 101eqtrd 2858 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → if(𝐼 = 𝐼, if((𝑄𝑗) = 𝐽, (1r𝑅), (0g𝑅)), (𝐼𝑀(𝑄𝑗))) = (0g𝑅))
10363, 74, 1023eqtrrd 2863 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) ∧ ¬ 𝑗 = 𝑁) → (0g𝑅) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
10458, 103ifeqda 4504 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ 𝑖 = 𝑁) → if(𝑗 = 𝑁, (1r𝑅), (0g𝑅)) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
105 simp2 1133 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
106105adantr 483 . . . . . . . . . 10 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑖 ∈ (1...𝑁))
10768adantr 483 . . . . . . . . . 10 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → 𝑗 ∈ (1...𝑁))
108 ovexd 7193 . . . . . . . . . 10 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) ∈ V)
10910oveqi 7171 . . . . . . . . . . . . . 14 ((𝑃𝑖)𝑈(𝑄𝑗)) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗))
110109a1i 11 . . . . . . . . . . . . 13 ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃𝑖)𝑈(𝑄𝑗)) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
111110mpoeq3ia 7234 . . . . . . . . . . . 12 (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)𝑈(𝑄𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
11217, 111eqtri 2846 . . . . . . . . . . 11 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
113112ovmpt4g 7299 . . . . . . . . . 10 ((𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁) ∧ ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)) ∈ V) → (𝑖𝑊𝑗) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
114106, 107, 108, 113syl3anc 1367 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑖 = 𝑁) → (𝑖𝑊𝑗) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
115104, 114ifeqda 4504 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r𝑅), (0g𝑅)), (𝑖𝑊𝑗)) = ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗)))
116115mpoeq3dva 7233 . . . . . . 7 (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r𝑅), (0g𝑅)), (𝑖𝑊𝑗))) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗))))
117 eqid 2823 . . . . . . . . . 10 (Base‘𝑅) = (Base‘𝑅)
118253ad2ant1 1129 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑃𝐺)
11969, 13symgfv 18510 . . . . . . . . . . . 12 ((𝑃𝐺𝑖 ∈ (1...𝑁)) → (𝑃𝑖) ∈ (1...𝑁))
120118, 105, 119syl2anc 586 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑃𝑖) ∈ (1...𝑁))
121243ad2ant1 1129 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑈𝐵)
1224, 117, 5, 120, 71, 121matecld 21037 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑃𝑖)𝑈(𝑄𝑗)) ∈ (Base‘𝑅))
1234, 117, 5, 19, 18, 122matbas2d 21034 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)𝑈(𝑄𝑗))) ∈ 𝐵)
12417, 123eqeltrid 2919 . . . . . . . 8 (𝜑𝑊𝐵)
125117, 48ringidcl 19320 . . . . . . . . 9 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
12621, 125syl 17 . . . . . . . 8 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
127 eqid 2823 . . . . . . . . 9 ((1...𝑁) matRRep 𝑅) = ((1...𝑁) matRRep 𝑅)
1284, 5, 127, 49marrepval 21173 . . . . . . . 8 (((𝑊𝐵 ∧ (1r𝑅) ∈ (Base‘𝑅)) ∧ (𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁))) → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r𝑅), (0g𝑅)), (𝑖𝑊𝑗))))
129124, 126, 91, 91, 128syl22anc 836 . . . . . . 7 (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁) = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ if(𝑖 = 𝑁, if(𝑗 = 𝑁, (1r𝑅), (0g𝑅)), (𝑖𝑊𝑗))))
130112a1i 11 . . . . . . 7 (𝜑𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃𝑖)(𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽)(𝑄𝑗))))
131116, 129, 1303eqtr4d 2868 . . . . . 6 (𝜑 → (𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁) = 𝑊)
132131fveq2d 6676 . . . . 5 (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = (𝐷𝑊))
133 eqid 2823 . . . . . . . . . . . 12 ((1...𝑁) subMat 𝑅) = ((1...𝑁) subMat 𝑅)
1344, 133, 5submaval 21192 . . . . . . . . . . 11 ((𝑊𝐵𝑁 ∈ (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
135124, 91, 91, 134syl3anc 1367 . . . . . . . . . 10 (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)))
136 fzdif2 30516 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
13789, 136syl 17 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
138 mpoeq12 7229 . . . . . . . . . . 11 ((((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)) ∧ ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
139137, 137, 138syl2anc 586 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ ((1...𝑁) ∖ {𝑁}), 𝑗 ∈ ((1...𝑁) ∖ {𝑁}) ↦ (𝑖𝑊𝑗)) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
140135, 139eqtrd 2858 . . . . . . . . 9 (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) = (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)))
141 difssd 4111 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁))
142137, 141eqsstrrd 4008 . . . . . . . . . 10 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1434, 5submabas 21189 . . . . . . . . . 10 ((𝑊𝐵 ∧ (1...(𝑁 − 1)) ⊆ (1...𝑁)) → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
144124, 142, 143syl2anc 586 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑁 − 1)), 𝑗 ∈ (1...(𝑁 − 1)) ↦ (𝑖𝑊𝑗)) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
145140, 144eqeltrd 2915 . . . . . . . 8 (𝜑 → (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅)))
146 madjusmdet.e . . . . . . . . 9 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅)
147 eqid 2823 . . . . . . . . 9 ((1...(𝑁 − 1)) Mat 𝑅) = ((1...(𝑁 − 1)) Mat 𝑅)
148 eqid 2823 . . . . . . . . 9 (Base‘((1...(𝑁 − 1)) Mat 𝑅)) = (Base‘((1...(𝑁 − 1)) Mat 𝑅))
149146, 147, 148, 117mdetcl 21207 . . . . . . . 8 ((𝑅 ∈ CRing ∧ (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁) ∈ (Base‘((1...(𝑁 − 1)) Mat 𝑅))) → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
15018, 145, 149syl2anc 586 . . . . . . 7 (𝜑 → (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅))
151117, 16, 48ringlidm 19323 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) ∈ (Base‘𝑅)) → ((1r𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
15221, 150, 151syl2anc 586 . . . . . 6 (𝜑 → ((1r𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
1534fveq2i 6675 . . . . . . . . . . 11 (Base‘𝐴) = (Base‘((1...𝑁) Mat 𝑅))
1545, 153eqtri 2846 . . . . . . . . . 10 𝐵 = (Base‘((1...𝑁) Mat 𝑅))
155124, 154eleqtrdi 2925 . . . . . . . . 9 (𝜑𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅)))
156 smadiadetr 21286 . . . . . . . . 9 (((𝑅 ∈ CRing ∧ 𝑊 ∈ (Base‘((1...𝑁) Mat 𝑅))) ∧ (𝑁 ∈ (1...𝑁) ∧ (1r𝑅) ∈ (Base‘𝑅))) → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅)(.r𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
15718, 155, 91, 126, 156syl22anc 836 . . . . . . . 8 (𝜑 → (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅)(.r𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
1586fveq1i 6673 . . . . . . . . 9 (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁))
15916oveqi 7171 . . . . . . . . 9 ((1r𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r𝑅)(.r𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
160158, 159eqeq12i 2838 . . . . . . . 8 ((𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) ↔ (((1...𝑁) maDet 𝑅)‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅)(.r𝑅)((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
161157, 160sylibr 236 . . . . . . 7 (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
162137oveq1d 7173 . . . . . . . . . 10 (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = ((1...(𝑁 − 1)) maDet 𝑅))
163162, 146syl6eqr 2876 . . . . . . . . 9 (𝜑 → (((1...𝑁) ∖ {𝑁}) maDet 𝑅) = 𝐸)
164163fveq1d 6674 . . . . . . . 8 (𝜑 → ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
165164oveq2d 7174 . . . . . . 7 (𝜑 → ((1r𝑅) · ((((1...𝑁) ∖ {𝑁}) maDet 𝑅)‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))) = ((1r𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
166161, 165eqtrd 2858 . . . . . 6 (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = ((1r𝑅) · (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))))
1674, 5submat1n 31072 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑊𝐵) → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
16887, 124, 167syl2anc 586 . . . . . . 7 (𝜑 → (𝑁(subMat1‘𝑊)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁))
169168fveq2d 6676 . . . . . 6 (𝜑 → (𝐸‘(𝑁(subMat1‘𝑊)𝑁)) = (𝐸‘(𝑁(((1...𝑁) subMat 𝑅)‘𝑊)𝑁)))
170152, 166, 1693eqtr4d 2868 . . . . 5 (𝜑 → (𝐷‘(𝑁(𝑊((1...𝑁) matRRep 𝑅)(1r𝑅))𝑁)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
171132, 170eqtr3d 2860 . . . 4 (𝜑 → (𝐷𝑊) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
1724, 5, 87, 3, 2, 21, 1, 10submatminr1 31077 . . . . . 6 (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝑈)𝐽))
173 madjusmdetlem1.3 . . . . . 6 (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
174172, 173eqtrd 2858 . . . . 5 (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝑁(subMat1‘𝑊)𝑁))
175174fveq2d 6676 . . . 4 (𝜑 → (𝐸‘(𝐼(subMat1‘𝑀)𝐽)) = (𝐸‘(𝑁(subMat1‘𝑊)𝑁)))
176171, 175eqtr4d 2861 . . 3 (𝜑 → (𝐷𝑊) = (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))
177176oveq2d 7174 . 2 (𝜑 → ((𝑍‘((𝑆𝑃) · (𝑆𝑄))) · (𝐷𝑊)) = ((𝑍‘((𝑆𝑃) · (𝑆𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))
17812, 27, 1773eqtrd 2862 1 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘((𝑆𝑃) · (𝑆𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))