axlowdimlem14

Description: Lemma for axlowdim . Take two possible Q from axlowdimlem10 . They are the same iff their distinguished values are the same. (Contributed by Scott Fenton, 21-Apr-2013)

	Ref	Expression
Hypotheses	axlowdimlem14.1	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
	axlowdimlem14.2	$⊢ R = \{⟨J + 1, 1⟩\} \cup (((1 \dots N) ∖ \{J + 1\}) \times \{0\})$
Assertion	axlowdimlem14	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (Q = R \to I = J)$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem14.1	$⊢ Q = \{⟨I + 1, 1⟩\} \cup (((1 \dots N) ∖ \{I + 1\}) \times \{0\})$
2		axlowdimlem14.2	$⊢ R = \{⟨J + 1, 1⟩\} \cup (((1 \dots N) ∖ \{J + 1\}) \times \{0\})$
3	1	axlowdimlem10	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to Q \in 𝔼 (N)$
4		elee	$⊢ N \in ℕ \to (Q \in 𝔼 (N) \leftrightarrow Q : (1 \dots N) ⟶ ℝ)$
5	4	adantr	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to (Q \in 𝔼 (N) \leftrightarrow Q : (1 \dots N) ⟶ ℝ)$
6	3 5	mpbid	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to Q : (1 \dots N) ⟶ ℝ$
7	6	ffnd	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to Q Fn (1 \dots N)$
8	2	axlowdimlem10	$⊢ (N \in ℕ \land J \in (1 \dots N - 1)) \to R \in 𝔼 (N)$
9		elee	$⊢ N \in ℕ \to (R \in 𝔼 (N) \leftrightarrow R : (1 \dots N) ⟶ ℝ)$
10	9	adantr	$⊢ (N \in ℕ \land J \in (1 \dots N - 1)) \to (R \in 𝔼 (N) \leftrightarrow R : (1 \dots N) ⟶ ℝ)$
11	8 10	mpbid	$⊢ (N \in ℕ \land J \in (1 \dots N - 1)) \to R : (1 \dots N) ⟶ ℝ$
12	11	ffnd	$⊢ (N \in ℕ \land J \in (1 \dots N - 1)) \to R Fn (1 \dots N)$
13		eqfnfv	$⊢ (Q Fn (1 \dots N) \land R Fn (1 \dots N)) \to (Q = R \leftrightarrow \forall i \in (1 \dots N) Q (i) = R (i))$
14	7 12 13	syl2an	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1)) \land (N \in ℕ \land J \in (1 \dots N - 1))) \to (Q = R \leftrightarrow \forall i \in (1 \dots N) Q (i) = R (i))$
15	14	3impdi	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (Q = R \leftrightarrow \forall i \in (1 \dots N) Q (i) = R (i))$
16		fznatpl1	$⊢ (N \in ℕ \land I \in (1 \dots N - 1)) \to I + 1 \in (1 \dots N)$
17	16	3adant3	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to I + 1 \in (1 \dots N)$
18		ax-1ne0	$⊢ 1 \neq 0$
19	18	a1i	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to 1 \neq 0$
20	1	axlowdimlem11	$⊢ Q (I + 1) = 1$
21	20	a1i	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to Q (I + 1) = 1$
22		elfzelz	$⊢ I \in (1 \dots N - 1) \to I \in ℤ$
23	22	zcnd	$⊢ I \in (1 \dots N - 1) \to I \in ℂ$
24		elfzelz	$⊢ J \in (1 \dots N - 1) \to J \in ℤ$
25	24	zcnd	$⊢ J \in (1 \dots N - 1) \to J \in ℂ$
26		ax-1cn	$⊢ 1 \in ℂ$
27		addcan2	$⊢ (I \in ℂ \land J \in ℂ \land 1 \in ℂ) \to (I + 1 = J + 1 \leftrightarrow I = J)$
28	26 27	mp3an3	$⊢ (I \in ℂ \land J \in ℂ) \to (I + 1 = J + 1 \leftrightarrow I = J)$
29	23 25 28	syl2an	$⊢ (I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (I + 1 = J + 1 \leftrightarrow I = J)$
30	29	3adant1	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (I + 1 = J + 1 \leftrightarrow I = J)$
31	30	necon3bid	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (I + 1 \neq J + 1 \leftrightarrow I \neq J)$
32	31	biimpar	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to I + 1 \neq J + 1$
33	2	axlowdimlem12	$⊢ (I + 1 \in (1 \dots N) \land I + 1 \neq J + 1) \to R (I + 1) = 0$
34	17 32 33	syl2an2r	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to R (I + 1) = 0$
35	19 21 34	3netr4d	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to Q (I + 1) \neq R (I + 1)$
36		df-ne	$⊢ Q (i) \neq R (i) \leftrightarrow \neg Q (i) = R (i)$
37		fveq2	$⊢ i = I + 1 \to Q (i) = Q (I + 1)$
38		fveq2	$⊢ i = I + 1 \to R (i) = R (I + 1)$
39	37 38	neeq12d	$⊢ i = I + 1 \to (Q (i) \neq R (i) \leftrightarrow Q (I + 1) \neq R (I + 1))$
40	36 39	syl5bbr	$⊢ i = I + 1 \to (\neg Q (i) = R (i) \leftrightarrow Q (I + 1) \neq R (I + 1))$
41	40	rspcev	$⊢ (I + 1 \in (1 \dots N) \land Q (I + 1) \neq R (I + 1)) \to \exists i \in (1 \dots N) \neg Q (i) = R (i)$
42	17 35 41	syl2an2r	$⊢ ((N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \land I \neq J) \to \exists i \in (1 \dots N) \neg Q (i) = R (i)$
43	42	ex	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (I \neq J \to \exists i \in (1 \dots N) \neg Q (i) = R (i))$
44		df-ne	$⊢ I \neq J \leftrightarrow \neg I = J$
45		rexnal	$⊢ \exists i \in (1 \dots N) \neg Q (i) = R (i) \leftrightarrow \neg \forall i \in (1 \dots N) Q (i) = R (i)$
46	43 44 45	3imtr3g	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (\neg I = J \to \neg \forall i \in (1 \dots N) Q (i) = R (i))$
47	46	con4d	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (\forall i \in (1 \dots N) Q (i) = R (i) \to I = J)$
48	15 47	sylbid	$⊢ (N \in ℕ \land I \in (1 \dots N - 1) \land J \in (1 \dots N - 1)) \to (Q = R \to I = J)$

Metamath Proof Explorer

Theorem axlowdimlem14

Proof