madjusmdetlem3

	Ref	Expression
Hypotheses	madjusmdet.b	$⊢ B = {Base}_{A}$
	madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
	madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
	madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
	madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	madjusmdet.z	$⊢ Z = ℤRHom (R)$
	madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
	madjusmdet.n	$⊢ φ \to N \in ℕ$
	madjusmdet.r	$⊢ φ \to R \in CRing$
	madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
	madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
	madjusmdet.m	$⊢ φ \to M \in B$
	madjusmdetlem2.p	$⊢ P = (i \in (1 \dots N) ⟼ if (i = 1, I, if (i \leq I, i - 1, i)))$
	madjusmdetlem2.s	$⊢ S = (i \in (1 \dots N) ⟼ if (i = 1, N, if (i \leq N, i - 1, i)))$
	madjusmdetlem4.q	$⊢ Q = (j \in (1 \dots N) ⟼ if (j = 1, J, if (j \leq J, j - 1, j)))$
	madjusmdetlem4.t	$⊢ T = (j \in (1 \dots N) ⟼ if (j = 1, N, if (j \leq N, j - 1, j)))$
	madjusmdetlem3.w	$⊢ W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j))$
	madjusmdetlem3.u	$⊢ φ \to U \in B$
Assertion	madjusmdetlem3	$⊢ φ \to I {subMat}_{1} (U) J = N {subMat}_{1} (W) N$

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	$⊢ B = {Base}_{A}$
2		madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
3		madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
4		madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
5		madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		madjusmdet.z	$⊢ Z = ℤRHom (R)$
7		madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
8		madjusmdet.n	$⊢ φ \to N \in ℕ$
9		madjusmdet.r	$⊢ φ \to R \in CRing$
10		madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
11		madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
12		madjusmdet.m	$⊢ φ \to M \in B$
13		madjusmdetlem2.p	$⊢ P = (i \in (1 \dots N) ⟼ if (i = 1, I, if (i \leq I, i - 1, i)))$
14		madjusmdetlem2.s	$⊢ S = (i \in (1 \dots N) ⟼ if (i = 1, N, if (i \leq N, i - 1, i)))$
15		madjusmdetlem4.q	$⊢ Q = (j \in (1 \dots N) ⟼ if (j = 1, J, if (j \leq J, j - 1, j)))$
16		madjusmdetlem4.t	$⊢ T = (j \in (1 \dots N) ⟼ if (j = 1, N, if (j \leq N, j - 1, j)))$
17		madjusmdetlem3.w	$⊢ W = (i \in (1 \dots N), j \in (1 \dots N) ⟼ (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j))$
18		madjusmdetlem3.u	$⊢ φ \to U \in B$
19		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
20	8 19	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
21		fzdif2	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
22	20 21	syl	$⊢ φ \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
23		difss	$⊢ (1 \dots N) ∖ \{N\} \subseteq (1 \dots N)$
24	22 23	eqsstrrdi	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
25	24	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (1 \dots N - 1) \subseteq (1 \dots N)$
26		simprl	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in (1 \dots N - 1)$
27	25 26	sseldd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in (1 \dots N)$
28		simprr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in (1 \dots N - 1)$
29	25 28	sseldd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in (1 \dots N)$
30		ovexd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j) \in V$
31	17	ovmpt4g	$⊢ (i \in (1 \dots N) \land j \in (1 \dots N) \land (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j) \in V) \to i W j = (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j)$
32	27 29 30 31	syl3anc	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i W j = (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j)$
33	26 28	ovresd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i ({W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}) j = i W j$
34		eqid	$⊢ I {subMat}_{1} (U) J = I {subMat}_{1} (U) J$
35	8	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to N \in ℕ$
36	10	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to I \in (1 \dots N)$
37	11	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to J \in (1 \dots N)$
38		eqid	$⊢ {Base}_{R} = {Base}_{R}$
39	2 38 1	matbas2i	$⊢ U \in B \to U \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
40	18 39	syl	$⊢ φ \to U \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
41	40	adantr	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to U \in ({Base}_{R}^{((1 \dots N) \times (1 \dots N))})$
42		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
43	42 27	sselid	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i \in ℕ$
44	42 29	sselid	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to j \in ℕ$
45		eqidd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) = if (i < I, i, i + 1)$
46		eqidd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (j < J, j, j + 1) = if (j < J, j, j + 1)$
47	34 35 35 36 37 41 43 44 45 46	smatlem	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i (I {subMat}_{1} (U) J) j = if (i < I, i, i + 1) U if (j < J, j, j + 1)$
48	1 2 3 4 5 6 7 8 9 10 10 12 13 14	madjusmdetlem2	$⊢ (φ \land i \in (1 \dots N - 1)) \to if (i < I, i, i + 1) = (P \circ S^{-1}) (i)$
49	26 48	syldan	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) = (P \circ S^{-1}) (i)$
50	1 2 3 4 5 6 7 8 9 11 11 12 15 16	madjusmdetlem2	$⊢ (φ \land j \in (1 \dots N - 1)) \to if (j < J, j, j + 1) = (Q \circ T^{-1}) (j)$
51	28 50	syldan	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (j < J, j, j + 1) = (Q \circ T^{-1}) (j)$
52	49 51	oveq12d	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to if (i < I, i, i + 1) U if (j < J, j, j + 1) = (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j)$
53	47 52	eqtrd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i (I {subMat}_{1} (U) J) j = (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j)$
54	32 33 53	3eqtr4rd	$⊢ (φ \land (i \in (1 \dots N - 1) \land j \in (1 \dots N - 1))) \to i (I {subMat}_{1} (U) J) j = i ({W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}) j$
55	54	ralrimivva	$⊢ φ \to \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (U) J) j = i ({W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}) j$
56		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
57	2 1 56 34 8 10 11 18	smatcl	$⊢ φ \to I {subMat}_{1} (U) J \in {Base}_{((1 \dots N - 1) Mat R)}$
58		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
59		eqid	$⊢ (1 \dots N) = (1 \dots N)$
60		eqid	$⊢ SymGrp ((1 \dots N)) = SymGrp ((1 \dots N))$
61		eqid	$⊢ {Base}_{SymGrp ((1 \dots N))} = {Base}_{SymGrp ((1 \dots N))}$
62	59 13 60 61	fzto1st	$⊢ I \in (1 \dots N) \to P \in {Base}_{SymGrp ((1 \dots N))}$
63	10 62	syl	$⊢ φ \to P \in {Base}_{SymGrp ((1 \dots N))}$
64		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
65	20 64	syl	$⊢ φ \to N \in (1 \dots N)$
66	59 14 60 61	fzto1st	$⊢ N \in (1 \dots N) \to S \in {Base}_{SymGrp ((1 \dots N))}$
67	65 66	syl	$⊢ φ \to S \in {Base}_{SymGrp ((1 \dots N))}$
68		eqid	$⊢ {inv}_{g} (SymGrp ((1 \dots N))) = {inv}_{g} (SymGrp ((1 \dots N)))$
69	60 61 68	symginv	$⊢ S \in {Base}_{SymGrp ((1 \dots N))} \to {inv}_{g} (SymGrp ((1 \dots N))) (S) = S^{-1}$
70	67 69	syl	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (S) = S^{-1}$
71	60	symggrp	$⊢ (1 \dots N) \in Fin \to SymGrp ((1 \dots N)) \in Grp$
72	58 71	syl	$⊢ φ \to SymGrp ((1 \dots N)) \in Grp$
73	61 68	grpinvcl	$⊢ (SymGrp ((1 \dots N)) \in Grp \land S \in {Base}_{SymGrp ((1 \dots N))}) \to {inv}_{g} (SymGrp ((1 \dots N))) (S) \in {Base}_{SymGrp ((1 \dots N))}$
74	72 67 73	syl2anc	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (S) \in {Base}_{SymGrp ((1 \dots N))}$
75	70 74	eqeltrrd	$⊢ φ \to S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
76		eqid	$⊢ +_{SymGrp ((1 \dots N))} = +_{SymGrp ((1 \dots N))}$
77	60 61 76	symgov	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P +_{SymGrp ((1 \dots N))} S^{-1} = P \circ S^{-1}$
78	60 61 76	symgcl	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P +_{SymGrp ((1 \dots N))} S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
79	77 78	eqeltrrd	$⊢ (P \in {Base}_{SymGrp ((1 \dots N))} \land S^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
80	63 75 79	syl2anc	$⊢ φ \to P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
81	80	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
82		simp2	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to i \in (1 \dots N)$
83	60 61	symgfv	$⊢ (P \circ S^{-1} \in {Base}_{SymGrp ((1 \dots N))} \land i \in (1 \dots N)) \to (P \circ S^{-1}) (i) \in (1 \dots N)$
84	81 82 83	syl2anc	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to (P \circ S^{-1}) (i) \in (1 \dots N)$
85	59 15 60 61	fzto1st	$⊢ J \in (1 \dots N) \to Q \in {Base}_{SymGrp ((1 \dots N))}$
86	11 85	syl	$⊢ φ \to Q \in {Base}_{SymGrp ((1 \dots N))}$
87	59 16 60 61	fzto1st	$⊢ N \in (1 \dots N) \to T \in {Base}_{SymGrp ((1 \dots N))}$
88	65 87	syl	$⊢ φ \to T \in {Base}_{SymGrp ((1 \dots N))}$
89	60 61 68	symginv	$⊢ T \in {Base}_{SymGrp ((1 \dots N))} \to {inv}_{g} (SymGrp ((1 \dots N))) (T) = T^{-1}$
90	88 89	syl	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (T) = T^{-1}$
91	61 68	grpinvcl	$⊢ (SymGrp ((1 \dots N)) \in Grp \land T \in {Base}_{SymGrp ((1 \dots N))}) \to {inv}_{g} (SymGrp ((1 \dots N))) (T) \in {Base}_{SymGrp ((1 \dots N))}$
92	72 88 91	syl2anc	$⊢ φ \to {inv}_{g} (SymGrp ((1 \dots N))) (T) \in {Base}_{SymGrp ((1 \dots N))}$
93	90 92	eqeltrrd	$⊢ φ \to T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
94	60 61 76	symgov	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q +_{SymGrp ((1 \dots N))} T^{-1} = Q \circ T^{-1}$
95	60 61 76	symgcl	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q +_{SymGrp ((1 \dots N))} T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
96	94 95	eqeltrrd	$⊢ (Q \in {Base}_{SymGrp ((1 \dots N))} \land T^{-1} \in {Base}_{SymGrp ((1 \dots N))}) \to Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
97	86 93 96	syl2anc	$⊢ φ \to Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
98	97	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))}$
99		simp3	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to j \in (1 \dots N)$
100	60 61	symgfv	$⊢ (Q \circ T^{-1} \in {Base}_{SymGrp ((1 \dots N))} \land j \in (1 \dots N)) \to (Q \circ T^{-1}) (j) \in (1 \dots N)$
101	98 99 100	syl2anc	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to (Q \circ T^{-1}) (j) \in (1 \dots N)$
102	18	3ad2ant1	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to U \in B$
103	2 38 1 84 101 102	matecld	$⊢ (φ \land i \in (1 \dots N) \land j \in (1 \dots N)) \to (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j) \in {Base}_{R}$
104	2 38 1 58 9 103	matbas2d	$⊢ φ \to (i \in (1 \dots N), j \in (1 \dots N) ⟼ (P \circ S^{-1}) (i) U (Q \circ T^{-1}) (j)) \in B$
105	17 104	eqeltrid	$⊢ φ \to W \in B$
106	2 1	submatres	$⊢ (N \in ℕ \land W \in B) \to N {subMat}_{1} (W) N = {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}$
107	8 105 106	syl2anc	$⊢ φ \to N {subMat}_{1} (W) N = {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}$
108		eqid	$⊢ N {subMat}_{1} (W) N = N {subMat}_{1} (W) N$
109	2 1 56 108 8 65 65 105	smatcl	$⊢ φ \to N {subMat}_{1} (W) N \in {Base}_{((1 \dots N - 1) Mat R)}$
110	107 109	eqeltrrd	$⊢ φ \to {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))} \in {Base}_{((1 \dots N - 1) Mat R)}$
111		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
112	111 56	eqmat	$⊢ (I {subMat}_{1} (U) J \in {Base}_{((1 \dots N - 1) Mat R)} \land {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))} \in {Base}_{((1 \dots N - 1) Mat R)}) \to (I {subMat}_{1} (U) J = {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))} \leftrightarrow \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (U) J) j = i ({W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}) j)$
113	57 110 112	syl2anc	$⊢ φ \to (I {subMat}_{1} (U) J = {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))} \leftrightarrow \forall i \in (1 \dots N - 1) \forall j \in (1 \dots N - 1) i (I {subMat}_{1} (U) J) j = i ({W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}) j)$
114	55 113	mpbird	$⊢ φ \to I {subMat}_{1} (U) J = {W ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}$
115	114 107	eqtr4d	$⊢ φ \to I {subMat}_{1} (U) J = N {subMat}_{1} (W) N$

Metamath Proof Explorer

Theorem madjusmdetlem3

Proof