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		simpr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x = X + 1$
38		1red	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 \in ℝ$
39		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
40		simpr	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in (1 \dots N - 1)$
41	39 40	sselid	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℕ$
42	41	nnrpd	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℝ^{+}$
43	42	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X \in ℝ^{+}$
44	38 43	ltaddrp2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 < X + 1$
45	38 44	gtned	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 \neq 1$
46	37 45	eqnetrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \neq 1$
47	46	neneqd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to \neg x = 1$
48	47	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)$
49	8	adantr	$⊢ (φ \land X \in (1 \dots N - 1)) \to N \in ℕ$
50	41	nnnn0d	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℕ_{0}$
51	49	nnnn0d	$⊢ (φ \land X \in (1 \dots N - 1)) \to N \in ℕ_{0}$
52		elfzle2	$⊢ X \in (1 \dots N - 1) \to X \leq N - 1$
53	40 52	syl	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \leq N - 1$
54		nn0ltlem1	$⊢ (X \in ℕ_{0} \land N \in ℕ_{0}) \to (X < N \leftrightarrow X \leq N - 1)$
55	54	biimpar	$⊢ ((X \in ℕ_{0} \land N \in ℕ_{0}) \land X \leq N - 1) \to X < N$
56	50 51 53 55	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to X < N$
57		nnltp1le	$⊢ (X \in ℕ \land N \in ℕ) \to (X < N \leftrightarrow X + 1 \leq N)$
58	57	biimpa	$⊢ ((X \in ℕ \land N \in ℕ) \land X < N) \to X + 1 \leq N$
59	41 49 56 58	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to X + 1 \leq N$
60	59	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 \leq N$
61	37 60	eqbrtrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \leq N$
62	61	iftrued	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to if (x \leq N, x - 1, x) = x - 1$
63	37	oveq1d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x - 1 = X + 1 - 1$
64	41	nncnd	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in ℂ$
65		1cnd	$⊢ (φ \land X \in (1 \dots N - 1)) \to 1 \in ℂ$
66	64 65	pncand	$⊢ (φ \land X \in (1 \dots N - 1)) \to X + 1 - 1 = X$
67	66	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to X + 1 - 1 = X$
68	63 67	eqtrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x - 1 = X$
69	48 62 68	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$
70	36 69 28 40	fvmptd2	$⊢ (φ \land X \in (1 \dots N - 1)) \to S (X + 1) = X$
71		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)$
72	71	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$
73	26 28 70 72	syl21anc	$⊢ (φ \land X \in (1 \dots N - 1)) \to S^{-1} (X) = X + 1$
74	73	fveq2d	$⊢ (φ \land X \in (1 \dots N - 1)) \to P (S^{-1} (X)) = P (X + 1)$
75	74	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to P (S^{-1} (X)) = P (X + 1)$
76		breq1	$⊢ i = x \to (i \leq I \leftrightarrow x \leq I)$
77	76 31 32	ifbieq12d	$⊢ i = x \to if (i \leq I, i - 1, i) = if (x \leq I, x - 1, x)$
78	29 77	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))$
79	78	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)))$
80	13 79	eqtri	$⊢ P = (x \in (1 \dots N) ⟼ if (x = 1, I, if (x \leq I, x - 1, x)))$
81	44 37	breqtrrd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to 1 < x$
82	38 81	gtned	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to x \neq 1$
83	82	neneqd	$⊢ ((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \to \neg x = 1$
84	83	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)$
85	84	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)$
86		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x = X + 1$
87	41	ad2antrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X \in ℕ$
88		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
89	88 10	sselid	$⊢ φ \to I \in ℕ$
90	89	ad3antrrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to I \in ℕ$
91		simplr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X < I$
92		nnltp1le	$⊢ (X \in ℕ \land I \in ℕ) \to (X < I \leftrightarrow X + 1 \leq I)$
93	92	biimpa	$⊢ ((X \in ℕ \land I \in ℕ) \land X < I) \to X + 1 \leq I$
94	87 90 91 93	syl21anc	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to X + 1 \leq I$
95	86 94	eqbrtrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x \leq I$
96	95	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$
97	68	adantlr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land X < I) \land x = X + 1) \to x - 1 = X$
98	85 96 97	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$
99	28	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X + 1 \in (1 \dots N)$
100		simplr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X \in (1 \dots N - 1)$
101	80 98 99 100	fvmptd2	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to P (X + 1) = X$
102	75 101	eqtr2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land X < I) \to X = P (S^{-1} (X))$
103	74	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to P (S^{-1} (X)) = P (X + 1)$
104	84	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)$
105	41	ad2antrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X \in ℕ$
106	89	ad3antrrr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to I \in ℕ$
107		simplr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to x = X + 1$
108		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to x \leq I$
109	107 108	eqbrtrrd	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X + 1 \leq I$
110	92	biimpar	$⊢ ((X \in ℕ \land I \in ℕ) \land X + 1 \leq I) \to X < I$
111	105 106 109 110	syl21anc	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land x \leq I) \to X < I$
112	111	stoic1a	$⊢ (((φ \land X \in (1 \dots N - 1)) \land x = X + 1) \land \neg X < I) \to \neg x \leq I$
113	112	an32s	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to \neg x \leq I$
114	113	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$
115		simpr	$⊢ (((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \land x = X + 1) \to x = X + 1$
116	104 114 115	3eqtrd	$⊢ (((φ \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$
117	28	adantr	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to X + 1 \in (1 \dots N)$
118	80 116 117 117	fvmptd2	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to P (X + 1) = X + 1$
119	103 118	eqtr2d	$⊢ ((φ \land X \in (1 \dots N - 1)) \land \neg X < I) \to X + 1 = P (S^{-1} (X))$
120	102 119	ifeqda	$⊢ (φ \land X \in (1 \dots N - 1)) \to if (X < I, X, X + 1) = P (S^{-1} (X))$
121		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)$
122	23 24 121	3syl	$⊢ φ \to S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
123		f1ofun	$⊢ S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun S^{-1}$
124	122 123	syl	$⊢ φ \to Fun S^{-1}$
125		fzdif2	$⊢ N \in ℤ_{\geq 1} \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
126	16 125	syl	$⊢ φ \to (1 \dots N) ∖ \{N\} = (1 \dots N - 1)$
127		difss	$⊢ (1 \dots N) ∖ \{N\} \subseteq (1 \dots N)$
128	126 127	eqsstrrdi	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
129		f1odm	$⊢ S^{-1} : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to dom S^{-1} = (1 \dots N)$
130	122 129	syl	$⊢ φ \to dom S^{-1} = (1 \dots N)$
131	128 130	sseqtrrd	$⊢ φ \to (1 \dots N - 1) \subseteq dom S^{-1}$
132	131	sselda	$⊢ (φ \land X \in (1 \dots N - 1)) \to X \in dom S^{-1}$
133		fvco	$⊢ (Fun S^{-1} \land X \in dom S^{-1}) \to (P \circ S^{-1}) (X) = P (S^{-1} (X))$
134	124 132 133	syl2an2r	$⊢ (φ \land X \in (1 \dots N - 1)) \to (P \circ S^{-1}) (X) = P (S^{-1} (X))$
135	120 134	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