Theorem 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	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
	axlowdimlem14.2	⊢ 𝑅 = ( { ⟨ ( 𝐽 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐽 + 1 ) } ) × { 0 } ) )
Assertion	axlowdimlem14	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 = 𝑅 → 𝐼 = 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem14.1	⊢ 𝑄 = ( { ⟨ ( 𝐼 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐼 + 1 ) } ) × { 0 } ) )
2		axlowdimlem14.2	⊢ 𝑅 = ( { ⟨ ( 𝐽 + 1 ) , 1 ⟩ } ∪ ( ( ( 1 ... 𝑁 ) ∖ { ( 𝐽 + 1 ) } ) × { 0 } ) )
3	1	axlowdimlem10	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
4		elee	⊢ ( 𝑁 ∈ ℕ → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
5	4	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
6	3 5	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 : ( 1 ... 𝑁 ) ⟶ ℝ )
7	6	ffnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑄 Fn ( 1 ... 𝑁 ) )
8	2	axlowdimlem10	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
9		elee	⊢ ( 𝑁 ∈ ℕ → ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑅 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
10	9	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑅 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
11	8 10	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑅 : ( 1 ... 𝑁 ) ⟶ ℝ )
12	11	ffnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑅 Fn ( 1 ... 𝑁 ) )
13		eqfnfv	⊢ ( ( 𝑄 Fn ( 1 ... 𝑁 ) ∧ 𝑅 Fn ( 1 ... 𝑁 ) ) → ( 𝑄 = 𝑅 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ) )
14	7 12 13	syl2an	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ( 𝑁 ∈ ℕ ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ) → ( 𝑄 = 𝑅 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ) )
15	14	3impdi	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 = 𝑅 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ) )
16		fznatpl1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) )
17	16	3adant3	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) )
18		ax-1ne0	⊢ 1 ≠ 0
19	18	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → 1 ≠ 0 )
20	1	axlowdimlem11	⊢ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 1
21	20	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 1 )
22		elfzelz	⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℤ )
23	22	zcnd	⊢ ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐼 ∈ ℂ )
24		elfzelz	⊢ ( 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐽 ∈ ℤ )
25	24	zcnd	⊢ ( 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝐽 ∈ ℂ )
26		ax-1cn	⊢ 1 ∈ ℂ
27		addcan2	⊢ ( ( 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐼 + 1 ) = ( 𝐽 + 1 ) ↔ 𝐼 = 𝐽 ) )
28	26 27	mp3an3	⊢ ( ( 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ) → ( ( 𝐼 + 1 ) = ( 𝐽 + 1 ) ↔ 𝐼 = 𝐽 ) )
29	23 25 28	syl2an	⊢ ( ( 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) = ( 𝐽 + 1 ) ↔ 𝐼 = 𝐽 ) )
30	29	3adant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) = ( 𝐽 + 1 ) ↔ 𝐼 = 𝐽 ) )
31	30	necon3bid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐼 + 1 ) ≠ ( 𝐽 + 1 ) ↔ 𝐼 ≠ 𝐽 ) )
32	31	biimpar	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 + 1 ) ≠ ( 𝐽 + 1 ) )
33	2	axlowdimlem12	⊢ ( ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝐼 + 1 ) ≠ ( 𝐽 + 1 ) ) → ( 𝑅 ‘ ( 𝐼 + 1 ) ) = 0 )
34	17 32 33	syl2an2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → ( 𝑅 ‘ ( 𝐼 + 1 ) ) = 0 )
35	19 21 34	3netr4d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ ( 𝑅 ‘ ( 𝐼 + 1 ) ) )
36		df-ne	⊢ ( ( 𝑄 ‘ 𝑖 ) ≠ ( 𝑅 ‘ 𝑖 ) ↔ ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) )
37		fveq2	⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
38		fveq2	⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ ( 𝐼 + 1 ) ) )
39	37 38	neeq12d	⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ≠ ( 𝑅 ‘ 𝑖 ) ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ ( 𝑅 ‘ ( 𝐼 + 1 ) ) ) )
40	36 39	bitr3id	⊢ ( 𝑖 = ( 𝐼 + 1 ) → ( ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ ( 𝑅 ‘ ( 𝐼 + 1 ) ) ) )
41	40	rspcev	⊢ ( ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝑁 ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≠ ( 𝑅 ‘ ( 𝐼 + 1 ) ) ) → ∃ 𝑖 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) )
42	17 35 41	syl2an2r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝐼 ≠ 𝐽 ) → ∃ 𝑖 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) )
43	42	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝐼 ≠ 𝐽 → ∃ 𝑖 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ) )
44		df-ne	⊢ ( 𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽 )
45		rexnal	⊢ ( ∃ 𝑖 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ↔ ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) )
46	43 44 45	3imtr3g	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ¬ 𝐼 = 𝐽 → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) ) )
47	46	con4d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑖 ) → 𝐼 = 𝐽 ) )
48	15 47	sylbid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∧ 𝐽 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑄 = 𝑅 → 𝐼 = 𝐽 ) )