Metamath Proof Explorer

Theorem vdwmc2

Description: Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwmc.1 ⊢ X ∈ V
vdwmc.2 ⊢ φ → K ∈ ℕ 0
vdwmc.3 ⊢ φ → F : X ⟶ R
vdwmc2.4 ⊢ φ → A ∈ X
Assertion vdwmc2 ⊢ φ → K MonoAP F ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c

Proof

Step Hyp Ref Expression
1 vdwmc.1 ⊢ X ∈ V
2 vdwmc.2 ⊢ φ → K ∈ ℕ 0
3 vdwmc.3 ⊢ φ → F : X ⟶ R
4 vdwmc2.4 ⊢ φ → A ∈ X
5 1 2 3 vdwmc ⊢ φ → K MonoAP F ↔ ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
6 vdwapid1 ⊢ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a ∈ a AP ⁡ K d
7 6 ne0d ⊢ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ≠ ∅
8 7 3expb ⊢ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ≠ ∅
9 8 adantll ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ≠ ∅
10 ssn0 ⊢ a AP ⁡ K d ⊆ F -1 c ∧ a AP ⁡ K d ≠ ∅ → F -1 c ≠ ∅
11 10 expcom ⊢ a AP ⁡ K d ≠ ∅ → a AP ⁡ K d ⊆ F -1 c → F -1 c ≠ ∅
12 9 11 syl ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ⊆ F -1 c → F -1 c ≠ ∅
13 disjsn ⊢ R ∩ c = ∅ ↔ ¬ c ∈ R
14 3 adantr ⊢ φ ∧ K ∈ ℕ → F : X ⟶ R
15 fimacnvdisj ⊢ F : X ⟶ R ∧ R ∩ c = ∅ → F -1 c = ∅
16 15 ex ⊢ F : X ⟶ R → R ∩ c = ∅ → F -1 c = ∅
17 14 16 syl ⊢ φ ∧ K ∈ ℕ → R ∩ c = ∅ → F -1 c = ∅
18 17 adantr ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → R ∩ c = ∅ → F -1 c = ∅
19 13 18 syl5bir ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → ¬ c ∈ R → F -1 c = ∅
20 19 necon1ad ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → F -1 c ≠ ∅ → c ∈ R
21 12 20 syld ⊢ φ ∧ K ∈ ℕ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ⊆ F -1 c → c ∈ R
22 21 rexlimdvva ⊢ φ ∧ K ∈ ℕ → ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c → c ∈ R
23 22 pm4.71rd ⊢ φ ∧ K ∈ ℕ → ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ c ∈ R ∧ ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
24 23 exbidv ⊢ φ ∧ K ∈ ℕ → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c c ∈ R ∧ ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
25 df-rex ⊢ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c c ∈ R ∧ ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
26 24 25 bitr4di ⊢ φ ∧ K ∈ ℕ → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
27 3 4 ffvelrnd ⊢ φ → F ⁡ A ∈ R
28 27 ne0d ⊢ φ → R ≠ ∅
29 1nn ⊢ 1 ∈ ℕ
30 29 ne0ii ⊢ ℕ ≠ ∅
31 simpllr ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → K = 0
32 31 fveq2d ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → AP ⁡ K = AP ⁡ 0
33 32 oveqd ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d = a AP ⁡ 0 d
34 vdwap0 ⊢ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ 0 d = ∅
35 34 adantll ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ 0 d = ∅
36 33 35 eqtrd ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d = ∅
37 0ss ⊢ ∅ ⊆ F -1 c
38 36 37 eqsstrdi ⊢ φ ∧ K = 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ⊆ F -1 c
39 38 ralrimiva ⊢ φ ∧ K = 0 ∧ a ∈ ℕ → ∀ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
40 r19.2z ⊢ ℕ ≠ ∅ ∧ ∀ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c → ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
41 30 39 40 sylancr ⊢ φ ∧ K = 0 ∧ a ∈ ℕ → ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
42 41 ralrimiva ⊢ φ ∧ K = 0 → ∀ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
43 r19.2z ⊢ ℕ ≠ ∅ ∧ ∀ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c → ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
44 30 42 43 sylancr ⊢ φ ∧ K = 0 → ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
45 44 ralrimivw ⊢ φ ∧ K = 0 → ∀ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
46 r19.2z ⊢ R ≠ ∅ ∧ ∀ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
47 28 45 46 syl2an2r ⊢ φ ∧ K = 0 → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
48 rexex ⊢ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
49 47 48 syl ⊢ φ ∧ K = 0 → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
50 49 47 2thd ⊢ φ ∧ K = 0 → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
51 elnn0 ⊢ K ∈ ℕ 0 ↔ K ∈ ℕ ∨ K = 0
52 2 51 sylib ⊢ φ → K ∈ ℕ ∨ K = 0
53 26 50 52 mpjaodan ⊢ φ → ∃ c ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c
54 vdwapval ⊢ K ∈ ℕ 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → x ∈ a AP ⁡ K d ↔ ∃ m ∈ 0 … K − 1 x = a + m ⁢ d
55 54 3expb ⊢ K ∈ ℕ 0 ∧ a ∈ ℕ ∧ d ∈ ℕ → x ∈ a AP ⁡ K d ↔ ∃ m ∈ 0 … K − 1 x = a + m ⁢ d
56 2 55 sylan ⊢ φ ∧ a ∈ ℕ ∧ d ∈ ℕ → x ∈ a AP ⁡ K d ↔ ∃ m ∈ 0 … K − 1 x = a + m ⁢ d
57 56 imbi1d ⊢ φ ∧ a ∈ ℕ ∧ d ∈ ℕ → x ∈ a AP ⁡ K d → x ∈ F -1 c ↔ ∃ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
58 57 albidv ⊢ φ ∧ a ∈ ℕ ∧ d ∈ ℕ → ∀ x x ∈ a AP ⁡ K d → x ∈ F -1 c ↔ ∀ x ∃ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
59 dfss2 ⊢ a AP ⁡ K d ⊆ F -1 c ↔ ∀ x x ∈ a AP ⁡ K d → x ∈ F -1 c
60 ralcom4 ⊢ ∀ m ∈ 0 … K − 1 ∀ x x = a + m ⁢ d → x ∈ F -1 c ↔ ∀ x ∀ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
61 ovex ⊢ a + m ⁢ d ∈ V
62 eleq1 ⊢ x = a + m ⁢ d → x ∈ F -1 c ↔ a + m ⁢ d ∈ F -1 c
63 61 62 ceqsalv ⊢ ∀ x x = a + m ⁢ d → x ∈ F -1 c ↔ a + m ⁢ d ∈ F -1 c
64 63 ralbii ⊢ ∀ m ∈ 0 … K − 1 ∀ x x = a + m ⁢ d → x ∈ F -1 c ↔ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c
65 r19.23v ⊢ ∀ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c ↔ ∃ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
66 65 albii ⊢ ∀ x ∀ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c ↔ ∀ x ∃ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
67 60 64 66 3bitr3i ⊢ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c ↔ ∀ x ∃ m ∈ 0 … K − 1 x = a + m ⁢ d → x ∈ F -1 c
68 58 59 67 3bitr4g ⊢ φ ∧ a ∈ ℕ ∧ d ∈ ℕ → a AP ⁡ K d ⊆ F -1 c ↔ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c
69 68 2rexbidva ⊢ φ → ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c
70 69 rexbidv ⊢ φ → ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ a AP ⁡ K d ⊆ F -1 c ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c
71 5 53 70 3bitrd ⊢ φ → K MonoAP F ↔ ∃ c ∈ R ∃ a ∈ ℕ ∃ d ∈ ℕ ∀ m ∈ 0 … K − 1 a + m ⁢ d ∈ F -1 c