Metamath Proof Explorer

Theorem unitscyglem3

Description: Lemma for unitscyg. (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 ⊢ B = Base G
unitscyglem1.2 ⊢ × ˙ = ⋅ G
unitscyglem1.3 ⊢ φ → G ∈ Grp
unitscyglem1.4 ⊢ φ → B ∈ Fin
unitscyglem1.5 ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n
Assertion unitscyglem3 ⊢ φ → ∀ d ∈ ℕ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 ⊢ B = Base G
2 unitscyglem1.2 ⊢ × ˙ = ⋅ G
3 unitscyglem1.3 ⊢ φ → G ∈ Grp
4 unitscyglem1.4 ⊢ φ → B ∈ Fin
5 unitscyglem1.5 ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n
6 breq1 ⊢ d = c → d ∥ B ↔ c ∥ B
7 eqeq2 ⊢ d = c → od ⁡ G ⁡ x = d ↔ od ⁡ G ⁡ x = c
8 7 rabbidv ⊢ d = c → x ∈ B | od ⁡ G ⁡ x = d = x ∈ B | od ⁡ G ⁡ x = c
9 8 neeq1d ⊢ d = c → x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ↔ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅
10 6 9 anbi12d ⊢ d = c → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ↔ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅
11 8 fveq2d ⊢ d = c → x ∈ B | od ⁡ G ⁡ x = d = x ∈ B | od ⁡ G ⁡ x = c
12 fveq2 ⊢ d = c → ϕ ⁡ d = ϕ ⁡ c
13 11 12 eqeq12d ⊢ d = c → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d ↔ x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
14 10 13 imbi12d ⊢ d = c → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d ↔ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
15 14 imbi2d ⊢ d = c → φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d ↔ φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
16 simplr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → φ
17 simplll ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → d ∈ ℕ
18 16 17 jca ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → φ ∧ d ∈ ℕ
19 breq1 ⊢ c = e → c < d ↔ e < d
20 breq1 ⊢ c = e → c ∥ B ↔ e ∥ B
21 eqeq2 ⊢ c = e → od ⁡ G ⁡ x = c ↔ od ⁡ G ⁡ x = e
22 21 rabbidv ⊢ c = e → x ∈ B | od ⁡ G ⁡ x = c = x ∈ B | od ⁡ G ⁡ x = e
23 22 neeq1d ⊢ c = e → x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅
24 20 23 anbi12d ⊢ c = e → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅
25 22 fveq2d ⊢ c = e → x ∈ B | od ⁡ G ⁡ x = c = x ∈ B | od ⁡ G ⁡ x = e
26 fveq2 ⊢ c = e → ϕ ⁡ c = ϕ ⁡ e
27 25 26 eqeq12d ⊢ c = e → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
28 24 27 imbi12d ⊢ c = e → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
29 28 imbi2d ⊢ c = e → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
30 19 29 imbi12d ⊢ c = e → c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
31 simpr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
32 31 adantr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ → ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
33 32 adantr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
34 33 adantr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ → ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
35 simpr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ → e ∈ ℕ
36 30 34 35 rspcdva ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ → e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
37 simp-5r ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ∧ e < d → φ
38 simpr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ∧ e < d → e < d
39 simplr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ∧ e < d → e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
40 38 39 mpd ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
41 37 40 mpd ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ∧ e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
42 41 ex ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ ∧ e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e → e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
43 42 ex ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ → e < d → φ → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e → e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
44 36 43 mpd ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ∧ e ∈ ℕ → e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
45 44 ralrimiva ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∀ e ∈ ℕ e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
46 nfv ⊢ Ⅎ c e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e
47 nfv ⊢ Ⅎ e c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
48 breq1 ⊢ e = c → e < d ↔ c < d
49 breq1 ⊢ e = c → e ∥ B ↔ c ∥ B
50 eqeq2 ⊢ e = c → od ⁡ G ⁡ x = e ↔ od ⁡ G ⁡ x = c
51 50 rabbidv ⊢ e = c → x ∈ B | od ⁡ G ⁡ x = e = x ∈ B | od ⁡ G ⁡ x = c
52 51 neeq1d ⊢ e = c → x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ ↔ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅
53 49 52 anbi12d ⊢ e = c → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ ↔ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅
54 51 fveq2d ⊢ e = c → x ∈ B | od ⁡ G ⁡ x = e = x ∈ B | od ⁡ G ⁡ x = c
55 fveq2 ⊢ e = c → ϕ ⁡ e = ϕ ⁡ c
56 54 55 eqeq12d ⊢ e = c → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ↔ x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
57 53 56 imbi12d ⊢ e = c → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ↔ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
58 48 57 imbi12d ⊢ e = c → e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ↔ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
59 46 47 58 cbvralw ⊢ ∀ e ∈ ℕ e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e ↔ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
60 59 biimpi ⊢ ∀ e ∈ ℕ e < d → e ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = e ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = e = ϕ ⁡ e → ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
61 45 60 syl ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
62 18 61 jca ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
63 simprl ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → d ∥ B
64 62 63 jca ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B
65 simprr ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d ≠ ∅
66 64 65 jca ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅
67 rabn0 ⊢ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ ↔ ∃ x ∈ B od ⁡ G ⁡ x = d
68 67 biimpi ⊢ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∃ x ∈ B od ⁡ G ⁡ x = d
69 68 adantl ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∃ x ∈ B od ⁡ G ⁡ x = d
70 simp-4l ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c
71 simp-4r ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → d ∥ B
72 simplr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → a ∈ B
73 70 71 72 jca31 ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B
74 simpr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → od ⁡ G ⁡ a = d
75 73 74 jca ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d
76 nfcv ⊢ Ⅎ _ x B
77 nfcv ⊢ Ⅎ _ z B
78 nfv ⊢ Ⅎ z od ⁡ G ⁡ x = d
79 nfv ⊢ Ⅎ x od ⁡ G ⁡ z = d
80 fveqeq2 ⊢ x = z → od ⁡ G ⁡ x = d ↔ od ⁡ G ⁡ z = d
81 76 77 78 79 80 cbvrabw ⊢ x ∈ B | od ⁡ G ⁡ x = d = z ∈ B | od ⁡ G ⁡ z = d
82 81 a1i ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → x ∈ B | od ⁡ G ⁡ x = d = z ∈ B | od ⁡ G ⁡ z = d
83 82 fveq2d ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → x ∈ B | od ⁡ G ⁡ x = d = z ∈ B | od ⁡ G ⁡ z = d
84 3 ad5antr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → G ∈ Grp
85 4 ad5antr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → B ∈ Fin
86 nfv ⊢ Ⅎ z n × ˙ x = 0 G
87 nfv ⊢ Ⅎ x n × ˙ z = 0 G
88 oveq2 ⊢ x = z → n × ˙ x = n × ˙ z
89 88 eqeq1d ⊢ x = z → n × ˙ x = 0 G ↔ n × ˙ z = 0 G
90 76 77 86 87 89 cbvrabw ⊢ x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
91 90 a1i ⊢ φ → x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
92 91 fveq2d ⊢ φ → x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
93 92 breq1d ⊢ φ → x ∈ B | n × ˙ x = 0 G ≤ n ↔ z ∈ B | n × ˙ z = 0 G ≤ n
94 93 ralbidv ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n ↔ ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
95 94 biimpd ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n → ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
96 5 95 mpd ⊢ φ → ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
97 96 ad5antr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
98 simp-5r ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → d ∈ ℕ
99 simpllr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → d ∥ B
100 simplr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → a ∈ B
101 simpr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → od ⁡ G ⁡ a = d
102 nfv ⊢ Ⅎ x od ⁡ G ⁡ z = c
103 nfv ⊢ Ⅎ z od ⁡ G ⁡ x = c
104 fveqeq2 ⊢ z = x → od ⁡ G ⁡ z = c ↔ od ⁡ G ⁡ x = c
105 77 76 102 103 104 cbvrabw ⊢ z ∈ B | od ⁡ G ⁡ z = c = x ∈ B | od ⁡ G ⁡ x = c
106 eqcom ⊢ z ∈ B | od ⁡ G ⁡ z = c = x ∈ B | od ⁡ G ⁡ x = c ↔ x ∈ B | od ⁡ G ⁡ x = c = z ∈ B | od ⁡ G ⁡ z = c
107 105 106 mpbi ⊢ x ∈ B | od ⁡ G ⁡ x = c = z ∈ B | od ⁡ G ⁡ z = c
108 107 neeq1i ⊢ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅
109 108 anbi2i ⊢ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅
110 107 fveq2i ⊢ x ∈ B | od ⁡ G ⁡ x = c = z ∈ B | od ⁡ G ⁡ z = c
111 110 eqeq1i ⊢ x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
112 109 111 imbi12i ⊢ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
113 112 imbi2i ⊢ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
114 113 biimpi ⊢ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
115 114 ralimi ⊢ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
116 115 adantl ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
117 116 adantr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
118 117 adantr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
119 118 adantr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
120 1 2 84 85 97 98 99 100 101 119 unitscyglem2 ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → z ∈ B | od ⁡ G ⁡ z = d = ϕ ⁡ d
121 83 120 eqtrd ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
122 75 121 syl ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d ∧ a ∈ B ∧ od ⁡ G ⁡ a = d → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
123 nfv ⊢ Ⅎ a od ⁡ G ⁡ x = d
124 nfv ⊢ Ⅎ x od ⁡ G ⁡ a = d
125 fveqeq2 ⊢ x = a → od ⁡ G ⁡ x = d ↔ od ⁡ G ⁡ a = d
126 123 124 125 cbvrexw ⊢ ∃ x ∈ B od ⁡ G ⁡ x = d ↔ ∃ a ∈ B od ⁡ G ⁡ a = d
127 126 biimpi ⊢ ∃ x ∈ B od ⁡ G ⁡ x = d → ∃ a ∈ B od ⁡ G ⁡ a = d
128 127 adantl ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d → ∃ a ∈ B od ⁡ G ⁡ a = d
129 122 128 r19.29a ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ ∃ x ∈ B od ⁡ G ⁡ x = d → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
130 129 ex ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B → ∃ x ∈ B od ⁡ G ⁡ x = d → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
131 130 adantr ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → ∃ x ∈ B od ⁡ G ⁡ x = d → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
132 69 131 mpd ⊢ φ ∧ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
133 66 132 syl ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ ∧ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
134 133 ex ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ∧ φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
135 134 ex ⊢ d ∈ ℕ ∧ ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
136 135 ex ⊢ d ∈ ℕ → ∀ c ∈ ℕ c < d → φ → c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c → φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
137 15 136 indstr ⊢ d ∈ ℕ → φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
138 137 com12 ⊢ φ → d ∈ ℕ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
139 138 imp ⊢ φ ∧ d ∈ ℕ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
140 139 ralrimiva ⊢ φ → ∀ d ∈ ℕ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d