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 bilani ⊢ φ ∧ 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
69 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
70 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
71 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
72 69 70 71 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
73 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
74 72 73 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
75 nfcv ⊢ Ⅎ _ x B
76 nfcv ⊢ Ⅎ _ z B
77 nfv ⊢ Ⅎ z od ⁡ G ⁡ x = d
78 nfv ⊢ Ⅎ x od ⁡ G ⁡ z = d
79 fveqeq2 ⊢ x = z → od ⁡ G ⁡ x = d ↔ od ⁡ G ⁡ z = d
80 75 76 77 78 79 cbvrabw ⊢ x ∈ B | od ⁡ G ⁡ x = d = z ∈ B | od ⁡ G ⁡ z = d
81 80 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
82 81 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
83 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
84 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
85 nfv ⊢ Ⅎ z n × ˙ x = 0 G
86 nfv ⊢ Ⅎ x n × ˙ z = 0 G
87 oveq2 ⊢ x = z → n × ˙ x = n × ˙ z
88 87 eqeq1d ⊢ x = z → n × ˙ x = 0 G ↔ n × ˙ z = 0 G
89 75 76 85 86 88 cbvrabw ⊢ x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
90 89 a1i ⊢ φ → x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
91 90 fveq2d ⊢ φ → x ∈ B | n × ˙ x = 0 G = z ∈ B | n × ˙ z = 0 G
92 91 breq1d ⊢ φ → x ∈ B | n × ˙ x = 0 G ≤ n ↔ z ∈ B | n × ˙ z = 0 G ≤ n
93 92 ralbidv ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n ↔ ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
94 93 biimpd ⊢ φ → ∀ n ∈ ℕ x ∈ B | n × ˙ x = 0 G ≤ n → ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
95 5 94 mpd ⊢ φ → ∀ n ∈ ℕ z ∈ B | n × ˙ z = 0 G ≤ n
96 95 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
97 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 ∈ ℕ
98 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
99 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
100 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
101 nfv ⊢ Ⅎ x od ⁡ G ⁡ z = c
102 nfv ⊢ Ⅎ z od ⁡ G ⁡ x = c
103 fveqeq2 ⊢ z = x → od ⁡ G ⁡ z = c ↔ od ⁡ G ⁡ x = c
104 76 75 101 102 103 cbvrabw ⊢ z ∈ B | od ⁡ G ⁡ z = c = x ∈ B | od ⁡ G ⁡ x = c
105 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
106 104 105 mpbi ⊢ x ∈ B | od ⁡ G ⁡ x = c = z ∈ B | od ⁡ G ⁡ z = c
107 106 neeq1i ⊢ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅
108 107 anbi2i ⊢ c ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = c ≠ ∅ ↔ c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅
109 106 fveq2i ⊢ x ∈ B | od ⁡ G ⁡ x = c = z ∈ B | od ⁡ G ⁡ z = c
110 109 eqeq1i ⊢ x ∈ B | od ⁡ G ⁡ x = c = ϕ ⁡ c ↔ z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
111 108 110 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
112 111 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
113 112 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
114 113 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
115 114 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
116 115 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
117 116 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
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 ∧ od ⁡ G ⁡ a = d → ∀ c ∈ ℕ c < d → c ∥ B ∧ z ∈ B | od ⁡ G ⁡ z = c ≠ ∅ → z ∈ B | od ⁡ G ⁡ z = c = ϕ ⁡ c
119 1 2 83 84 96 97 98 99 100 118 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
120 82 119 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
121 74 120 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
122 nfv ⊢ Ⅎ a od ⁡ G ⁡ x = d
123 nfv ⊢ Ⅎ x od ⁡ G ⁡ a = d
124 fveqeq2 ⊢ x = a → od ⁡ G ⁡ x = d ↔ od ⁡ G ⁡ a = d
125 122 123 124 cbvrexw ⊢ ∃ x ∈ B od ⁡ G ⁡ x = d ↔ ∃ a ∈ B od ⁡ G ⁡ a = d
126 125 bilani ⊢ φ ∧ 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
127 121 126 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
128 127 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
129 128 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
130 68 129 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
131 66 130 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
132 131 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
133 132 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
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 15 134 indstr ⊢ d ∈ ℕ → φ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
136 135 com12 ⊢ φ → d ∈ ℕ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
137 136 imp ⊢ φ ∧ d ∈ ℕ → d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d
138 137 ralrimiva ⊢ φ → ∀ d ∈ ℕ d ∥ B ∧ x ∈ B | od ⁡ G ⁡ x = d ≠ ∅ → x ∈ B | od ⁡ G ⁡ x = d = ϕ ⁡ d