madjusmdetlem2

	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)))$
Assertion	madjusmdetlem2	$⊢ (φ \land X \in (1 \dots N - 1)) \to if (X < I, X, X + 1) = (P \circ S^{-1}) (X)$

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		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16	8 15	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
17		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
18	16 17	syl	$⊢ φ \to N \in (1 \dots N)$
19		eqid	$⊢ (1 \dots N) = (1 \dots N)$
20		eqid	$⊢ SymGrp ((1 \dots N)) = SymGrp ((1 \dots N))$
21		eqid	$⊢ {Base}_{SymGrp ((1 \dots N))} = {Base}_{SymGrp ((1 \dots N))}$
22	19 14 20 21	fzto1st	$⊢ N \in (1 \dots N) \to S \in {Base}_{SymGrp ((1 \dots N))}$
23	18 22	syl	$⊢ φ \to S \in {Base}_{SymGrp ((1 \dots N))}$
24	20 21	symgbasf1o	$⊢ S \in {Base}_{SymGrp ((1 \dots N))} \to S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
25	23 24	syl	$⊢ φ \to S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
26	25	adantr	$⊢ (φ \land X \in (1 \dots N - 1)) \to S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
27		fznatpl1	$⊢ (N \in ℕ \land X \in (1 \dots N - 1)) \to X + 1 \in (1 \dots N)$
28	8 27	sylan	$⊢ (φ \land X \in (1 \dots N - 1)) \to X + 1 \in (1 \dots N)$
29		eqeq1	$⊢ i = x \to (i = 1 \leftrightarrow x = 1)$
30		breq1	$⊢ i = x \to (i \leq N \leftrightarrow x \leq N)$
31		oveq1	$⊢ i = x \to i - 1 = x - 1$
32		id	$⊢ i = x \to i = x$
33	30 31 32	ifbieq12d	$⊢ i = x \to if (i \leq N, i - 1, i) = if (x \leq N, x - 1, x)$
34	29 33	ifbieq2d	$⊢ i = x \to if (i = 1, N, if (i \leq N, i - 1, i)) = if (x = 1, N, if (x \leq N, x - 1, x))$
35	34	cbvmptv	$⊢ (i \in (1 \dots N) ⟼ if (i = 1, N, if (i \leq N, i - 1, i))) = (x \in (1 \dots N) ⟼ if (x = 1, N, if (x \leq N, x - 1, x)))$
36	14 35	eqtri	$⊢ S = (x \in (1 \dots N) ⟼ if (x = 1, N, if (x \leq N, x - 1, x)))$
37	36	a1i	$⊢ (φ \land X \in (1 \dots N - 1)) \to S = (x \in (1 \dots N) ⟼ if (x = 1, N, if (x \leq N, x - 1, x)))$
38		simpr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x = X + 1$
39		1red	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 \in ℝ$
40		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
41		simpr	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in (1 \dots N - 1)$
42	40 41	sselid	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℕ$
43	42	nnrpd	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℝ^{+}$
44	43	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X \in ℝ^{+}$
45	39 44	ltaddrp2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 < X + 1$
46	39 45	ltned	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 \neq X + 1$
47	46	necomd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 \neq 1$
48	38 47	eqnetrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \neq 1$
49	48	neneqd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to \neg x = 1$
50	49	iffalsed	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to if (x = 1, N, if (x \leq N, x - 1, x)) = if (x \leq N, x - 1, x)$
51	8	adantr	$⊢ (φ \land X \in (1 \dots N - 1)) \to N \in ℕ$
52	42	nnnn0d	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℕ_{0}$
53	51	nnnn0d	$⊢ (φ \land X \in (1 \dots N - 1)) \to N \in ℕ_{0}$
54		elfzle2	$⊢ X \in (1 \dots N - 1) \to X \leq N - 1$
55	41 54	syl	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \leq N - 1$
56		nn0ltlem1	$⊢ (X \in ℕ_{0} \land N \in ℕ_{0}) \to (X < N \leftrightarrow X \leq N - 1)$
57	56	biimpar	$⊢ ((X \in ℕ_{0} \land N \in ℕ_{0}) \land X \leq N - 1) \to X < N$
58	52 53 55 57	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to X < N$
59		nnltp1le	$⊢ (X \in ℕ \land N \in ℕ) \to (X < N \leftrightarrow X + 1 \leq N)$
60	59	biimpa	$⊢ ((X \in ℕ \land N \in ℕ) \land X < N) \to X + 1 \leq N$
61	42 51 58 60	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to X + 1 \leq N$
62	61	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 \leq N$
63	38 62	eqbrtrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \leq N$
64	63	iftrued	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to if (x \leq N, x - 1, x) = x - 1$
65	38	oveq1d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x - 1 = X + 1 - 1$
66	42	nncnd	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℂ$
67		1cnd	$⊢ (φ \land X \in (1 \dots N - 1)) \to 1 \in ℂ$
68	66 67	pncand	$⊢ (φ \land X \in (1 \dots N - 1)) \to X + 1 - 1 = X$
69	68	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 - 1 = X$
70	65 69	eqtrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x - 1 = X$
71	50 64 70	3eqtrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to if (x = 1, N, if (x \leq N, x - 1, x)) = X$
72	37 71 28 41	fvmptd	$⊢ (φ \land X \in (1 \dots N - 1)) \to S (X + 1) = X$
73	72	idi	$⊢ (φ \land X \in (1 \dots N - 1)) \to S (X + 1) = X$
74		f1ocnvfv	$⊢ (S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land X + 1 \in (1 \dots N)) \to (S (X + 1) = X \to S^{-1} (X) = X + 1)$
75	74	imp	$⊢ ((S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \land X + 1 \in (1 \dots N)) \land S (X + 1) = X) \to S^{-1} (X) = X + 1$
76	26 28 73 75	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to S^{-1} (X) = X + 1$
77	76	fveq2d	$⊢ (φ \land X \in (1 \dots N - 1)) \to P (S^{-1} (X)) = P (X + 1)$
78	77	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to P (S^{-1} (X)) = P (X + 1)$
79	32	breq1d	$⊢ i = x \to (i \leq I \leftrightarrow x \leq I)$
80	79 31 32	ifbieq12d	$⊢ i = x \to if (i \leq I, i - 1, i) = if (x \leq I, x - 1, x)$
81	29 80	ifbieq2d	$⊢ i = x \to if (i = 1, I, if (i \leq I, i - 1, i)) = if (x = 1, I, if (x \leq I, x - 1, x))$
82	81	cbvmptv	$⊢ (i \in (1 \dots N) ⟼ if (i = 1, I, if (i \leq I, i - 1, i))) = (x \in (1 \dots N) ⟼ if (x = 1, I, if (x \leq I, x - 1, x)))$
83	13 82	eqtri	$⊢ P = (x \in (1 \dots N) ⟼ if (x = 1, I, if (x \leq I, x - 1, x)))$
84	83	a1i	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to P = (x \in (1 \dots N) ⟼ if (x = 1, I, if (x \leq I, x - 1, x)))$
85	45 38	breqtrrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 < x$
86	39 85	ltned	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 \neq x$
87	86	necomd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \neq 1$
88	87	neneqd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to \neg x = 1$
89	88	iffalsed	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to if (x = 1, I, if (x \leq I, x - 1, x)) = if (x \leq I, x - 1, x)$
90	89	adantlr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to if (x = 1, I, if (x \leq I, x - 1, x)) = if (x \leq I, x - 1, x)$
91		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x = X + 1$
92	42	ad2antrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X \in ℕ$
93		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
94	93 10	sselid	$⊢ φ \to I \in ℕ$
95	94	ad3antrrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to I \in ℕ$
96		simplr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X < I$
97		nnltp1le	$⊢ (X \in ℕ \land I \in ℕ) \to (X < I \leftrightarrow X + 1 \leq I)$
98	97	biimpa	$⊢ ((X \in ℕ \land I \in ℕ) \land X < I) \to X + 1 \leq I$
99	92 95 96 98	syl21anc	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X + 1 \leq I$
100	91 99	eqbrtrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x \leq I$
101	100	iftrued	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to if (x \leq I, x - 1, x) = x - 1$
102	70	adantlr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x - 1 = X$
103	90 101 102	3eqtrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to if (x = 1, I, if (x \leq I, x - 1, x)) = X$
104	28	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X + 1 \in (1 \dots N)$
105		simplr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X \in (1 \dots N - 1)$
106	84 103 104 105	fvmptd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to P (X + 1) = X$
107	78 106	eqtr2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X = P (S^{-1} (X))$
108	77	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to P (S^{-1} (X)) = P (X + 1)$
109	83	a1i	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to P = (x \in (1 \dots N) ⟼ if (x = 1, I, if (x \leq I, x - 1, x)))$
110	89	adantlr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to if (x = 1, I, if (x \leq I, x - 1, x)) = if (x \leq I, x - 1, x)$
111	42	ad2antrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X \in ℕ$
112	94	ad3antrrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to I \in ℕ$
113	38	adantr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to x = X + 1$
114		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to x \leq I$
115	113 114	eqbrtrrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X + 1 \leq I$
116	97	biimpar	$⊢ ((X \in ℕ \land I \in ℕ) \land X + 1 \leq I) \to X < I$
117	111 112 115 116	syl21anc	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X < I$
118	117	ex	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to (x \leq I \to X < I)$
119	118	con3d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to (\neg X < I \to \neg x \leq I)$
120	119	imp	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land \neg X < I) \to \neg x \leq I$
121	120	an32s	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to \neg x \leq I$
122	121	iffalsed	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to if (x \leq I, x - 1, x) = x$
123		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to x = X + 1$
124	122 123	eqtrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to if (x \leq I, x - 1, x) = X + 1$
125	110 124	eqtrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to if (x = 1, I, if (x \leq I, x - 1, x)) = X + 1$
126	28	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to X + 1 \in (1 \dots N)$
127	109 125 126 126	fvmptd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to P (X + 1) = X + 1$
128	108 127	eqtr2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to X + 1 = P (S^{-1} (X))$
129	107 128	ifeqda	$⊢ (φ \land X \in (1 \dots N - 1)) \to if (X < I, X, X + 1) = P (S^{-1} (X))$
130		f1ocnv	$⊢ S : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
131	23 24 130	3syl	$⊢ φ \to S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
132		f1ofun	$⊢ S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun S^{-1}$
133	131 132	syl	$⊢ φ \to Fun S^{-1}$
134	133	adantr	$⊢ (φ \land X \in (1 \dots N - 1)) \to Fun S^{-1}$
135		fzdif2	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
136	16 135	syl	$⊢ φ \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
137		difss	$⊢ (1 \dots N) ∖ \{N\} \subseteq (1 \dots N)$
138	136 137	eqsstrrdi	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
139		f1odm	$⊢ S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to dom S^{-1} = (1 \dots N)$
140	131 139	syl	$⊢ φ \to dom S^{-1} = (1 \dots N)$
141	138 140	sseqtrrd	$⊢ φ \to (1 \dots N - 1) \subseteq dom S^{-1}$
142	141	adantr	$⊢ (φ \land X \in (1 \dots N - 1)) \to (1 \dots N - 1) \subseteq dom S^{-1}$
143	142 41	sseldd	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in dom S^{-1}$
144		fvco	$⊢ (Fun S^{-1} \land X \in dom S^{-1}) \to (P \circ S^{-1}) (X) = P (S^{-1} (X))$
145	134 143 144	syl2anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to (P \circ S^{-1}) (X) = P (S^{-1} (X))$
146	129 145	eqtr4d	$⊢ (φ \land X \in (1 \dots N - 1)) \to if (X < I, X, X + 1) = (P \circ S^{-1}) (X)$

Metamath Proof Explorer

Theorem madjusmdetlem2

Proof