Metamath Proof Explorer

Theorem smndex1basss

Description: The modulo function I and the constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
smndex1ibas.n ⊢ N ∈ ℕ
smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
Assertion smndex1basss ⊢ B ⊆ Base M

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex1ibas.n ⊢ N ∈ ℕ
3 smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
4 smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
5 smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
6 5 eleq2i ⊢ b ∈ B ↔ b ∈ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
7 fveq2 ⊢ n = k → G ⁡ n = G ⁡ k
8 7 sneqd ⊢ n = k → G ⁡ n = G ⁡ k
9 8 cbviunv ⊢ ⋃ n ∈ 0 ..^ N G ⁡ n = ⋃ k ∈ 0 ..^ N G ⁡ k
10 9 uneq2i ⊢ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n = I ∪ ⋃ k ∈ 0 ..^ N G ⁡ k
11 10 eleq2i ⊢ b ∈ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n ↔ b ∈ I ∪ ⋃ k ∈ 0 ..^ N G ⁡ k
12 6 11 bitri ⊢ b ∈ B ↔ b ∈ I ∪ ⋃ k ∈ 0 ..^ N G ⁡ k
13 elun ⊢ b ∈ I ∪ ⋃ k ∈ 0 ..^ N G ⁡ k ↔ b ∈ I ∨ b ∈ ⋃ k ∈ 0 ..^ N G ⁡ k
14 velsn ⊢ b ∈ I ↔ b = I
15 eliun ⊢ b ∈ ⋃ k ∈ 0 ..^ N G ⁡ k ↔ ∃ k ∈ 0 ..^ N b ∈ G ⁡ k
16 14 15 orbi12i ⊢ b ∈ I ∨ b ∈ ⋃ k ∈ 0 ..^ N G ⁡ k ↔ b = I ∨ ∃ k ∈ 0 ..^ N b ∈ G ⁡ k
17 12 13 16 3bitri ⊢ b ∈ B ↔ b = I ∨ ∃ k ∈ 0 ..^ N b ∈ G ⁡ k
18 1 2 3 smndex1ibas ⊢ I ∈ Base M
19 eleq1 ⊢ b = I → b ∈ Base M ↔ I ∈ Base M
20 18 19 mpbiri ⊢ b = I → b ∈ Base M
21 1 2 3 4 smndex1gbas ⊢ k ∈ 0 ..^ N → G ⁡ k ∈ Base M
22 21 adantr ⊢ k ∈ 0 ..^ N ∧ b ∈ G ⁡ k → G ⁡ k ∈ Base M
23 elsni ⊢ b ∈ G ⁡ k → b = G ⁡ k
24 23 eleq1d ⊢ b ∈ G ⁡ k → b ∈ Base M ↔ G ⁡ k ∈ Base M
25 24 adantl ⊢ k ∈ 0 ..^ N ∧ b ∈ G ⁡ k → b ∈ Base M ↔ G ⁡ k ∈ Base M
26 22 25 mpbird ⊢ k ∈ 0 ..^ N ∧ b ∈ G ⁡ k → b ∈ Base M
27 26 rexlimiva ⊢ ∃ k ∈ 0 ..^ N b ∈ G ⁡ k → b ∈ Base M
28 20 27 jaoi ⊢ b = I ∨ ∃ k ∈ 0 ..^ N b ∈ G ⁡ k → b ∈ Base M
29 17 28 sylbi ⊢ b ∈ B → b ∈ Base M
30 29 ssriv ⊢ B ⊆ Base M