Metamath Proof Explorer

Theorem grpods

Description: Relate sums of elements of orders and roots of unity. (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses grpods.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
grpods.2 ⊢ ↑ = ( .g ‘ 𝐺 )
grpods.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
grpods.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
grpods.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion grpods ( 𝜑 → Σ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )

Proof

Step Hyp Ref Expression
1 grpods.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 grpods.2 ⊢ ↑ = ( .g ‘ 𝐺 )
3 grpods.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 grpods.4 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 grpods.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑁 ↑ 𝑥 ) = ( 𝑁 ↑ 𝑦 ) )
7 6 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
8 7 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
9 8 biimpi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } → ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) → ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
11 simpl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝜑 )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑦 ∈ 𝐵 )
13 11 12 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
15 11 3 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝐺 ∈ Grp )
16 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝐺 ∈ Mnd )
18 11 5 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑁 ∈ ℕ )
19 18 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑁 ∈ ℕ0 )
20 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
21 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
22 1 20 2 21 oddvdsnn0 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ↔ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
23 17 12 19 22 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ↔ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
24 14 23 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 )
25 13 24 jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) )
26 breq1 ⊢ ( 𝑚 = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) → ( 𝑚 ∥ 𝑁 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) )
27 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 1 ∈ ℤ )
28 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝑁 ∈ ℕ )
29 28 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝑁 ∈ ℤ )
30 dvdszrcl ⊢ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
31 30 simpld ⊢ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ )
33 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝐺 ∈ Grp )
34 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝐵 ∈ Fin )
35 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝑦 ∈ 𝐵 )
36 1 20 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑦 ∈ 𝐵 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℕ )
37 33 34 35 36 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℕ )
38 37 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 1 ≤ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) )
39 32 28 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 )
41 dvdsle ⊢ ( ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ≤ 𝑁 ) )
42 41 imp ⊢ ( ( ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ≤ 𝑁 )
43 39 40 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ≤ 𝑁 )
44 27 29 32 38 43 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 1 ... 𝑁 ) )
45 26 44 40 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } )
46 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) )
47 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) )
48 46 35 47 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) } )
49 eqeq2 ⊢ ( 𝑘 = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) )
50 49 rabbidv ⊢ ( 𝑘 = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) } )
51 50 eliuni ⊢ ( ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ 𝐺 ) ‘ 𝑦 ) } ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
52 45 48 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∥ 𝑁 ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
53 25 52 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
54 53 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
56 10 55 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
57 56 ex ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } → 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
58 eliun ⊢ ( 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ↔ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
59 58 biimpi ⊢ ( 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } → ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) → ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
61 simplll ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝜑 )
62 simplr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } )
63 61 62 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } )
65 63 64 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) )
66 elrabi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } → 𝑦 ∈ 𝐵 )
67 66 adantl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝑦 ∈ 𝐵 )
68 simpll ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝜑 )
69 breq1 ⊢ ( 𝑚 = 𝑙 → ( 𝑚 ∥ 𝑁 ↔ 𝑙 ∥ 𝑁 ) )
70 69 elrab ⊢ ( 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ↔ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) )
71 70 biimpi ⊢ ( 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } → ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) )
72 71 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) )
74 68 73 jca ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) )
75 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) )
76 75 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ↔ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) )
77 76 biimpi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } → ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) )
78 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) )
79 74 78 jca ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) )
80 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → 𝜑 )
81 simprr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → 𝑙 ∥ 𝑁 )
82 elfzelz ⊢ ( 𝑙 ∈ ( 1 ... 𝑁 ) → 𝑙 ∈ ℤ )
83 82 adantr ⊢ ( ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) → 𝑙 ∈ ℤ )
84 83 adantl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → 𝑙 ∈ ℤ )
85 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → 𝑁 ∈ ℕ )
86 85 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → 𝑁 ∈ ℤ )
87 divides ⊢ ( ( 𝑙 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑙 ∥ 𝑁 ↔ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) )
88 84 86 87 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → ( 𝑙 ∥ 𝑁 ↔ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) )
89 81 88 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) → ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 )
90 89 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 )
91 80 90 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) )
92 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) )
93 91 92 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) )
94 oveq1 ⊢ ( ( 𝑑 · 𝑙 ) = 𝑁 → ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) = ( 𝑁 ↑ 𝑦 ) )
95 94 eqcomd ⊢ ( ( 𝑑 · 𝑙 ) = 𝑁 → ( 𝑁 ↑ 𝑦 ) = ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) )
96 95 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) ∧ ( 𝑑 · 𝑙 ) = 𝑁 ) → ( 𝑁 ↑ 𝑦 ) = ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) )
97 simplrr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 )
98 97 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑑 · 𝑙 ) )
99 98 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 · 𝑙 ) = ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) )
100 99 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) = ( ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) ↑ 𝑦 ) )
101 simplll ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → 𝜑 )
102 simplrl ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → 𝑦 ∈ 𝐵 )
103 101 102 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) )
104 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → 𝑑 ∈ ℤ )
105 103 104 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) )
106 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → 𝐺 ∈ Grp )
107 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → 𝑑 ∈ ℤ )
108 1 20 odcl ⊢ ( 𝑦 ∈ 𝐵 → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℕ0 )
109 108 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℕ0 )
110 109 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ )
111 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → 𝑦 ∈ 𝐵 )
112 107 110 111 3jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑦 ∈ 𝐵 ) )
113 1 2 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑑 ∈ ℤ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ∈ ℤ ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) ↑ 𝑦 ) = ( 𝑑 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) ) )
114 106 112 113 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) ↑ 𝑦 ) = ( 𝑑 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) ) )
115 1 20 2 21 odid ⊢ ( 𝑦 ∈ 𝐵 → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
116 111 115 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
117 116 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) ) = ( 𝑑 ↑ ( 0g ‘ 𝐺 ) ) )
118 1 2 21 mulgz ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
119 106 107 118 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ↑ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
120 117 119 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( 𝑑 ↑ ( ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ↑ 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
121 114 120 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
122 105 121 syl ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝑑 · ( ( od ‘ 𝐺 ) ‘ 𝑦 ) ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
123 100 122 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) → ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
124 123 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) ∧ ( 𝑑 · 𝑙 ) = 𝑁 ) → ( ( 𝑑 · 𝑙 ) ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
125 96 124 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) ∧ 𝑑 ∈ ℤ ) ∧ ( 𝑑 · 𝑙 ) = 𝑁 ) → ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
126 nfv ⊢ Ⅎ 𝑑 ( 𝑐 · 𝑙 ) = 𝑁
127 nfv ⊢ Ⅎ 𝑐 ( 𝑑 · 𝑙 ) = 𝑁
128 oveq1 ⊢ ( 𝑐 = 𝑑 → ( 𝑐 · 𝑙 ) = ( 𝑑 · 𝑙 ) )
129 128 eqeq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 · 𝑙 ) = 𝑁 ↔ ( 𝑑 · 𝑙 ) = 𝑁 ) )
130 126 127 129 cbvrexw ⊢ ( ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ↔ ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑙 ) = 𝑁 )
131 130 biimpi ⊢ ( ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 → ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑙 ) = 𝑁 )
132 131 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) → ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑙 ) = 𝑁 )
133 132 adantr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑙 ) = 𝑁 )
134 125 133 r19.29a ⊢ ( ( ( 𝜑 ∧ ∃ 𝑐 ∈ ℤ ( 𝑐 · 𝑙 ) = 𝑁 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
135 93 134 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑙 ∥ 𝑁 ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑦 ) = 𝑙 ) ) → ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
136 79 135 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → ( 𝑁 ↑ 𝑦 ) = ( 0g ‘ 𝐺 ) )
137 7 67 136 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
138 65 137 syl ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) ∧ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
139 nfv ⊢ Ⅎ 𝑙 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 }
140 nfv ⊢ Ⅎ 𝑘 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 }
141 eqeq2 ⊢ ( 𝑘 = 𝑙 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 ) )
142 141 rabbidv ⊢ ( 𝑘 = 𝑙 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } )
143 142 eleq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ↔ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } ) )
144 139 140 143 cbvrexw ⊢ ( ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ↔ ∃ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } )
145 144 biimpi ⊢ ( ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } → ∃ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } )
146 145 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) → ∃ 𝑙 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑙 } )
147 138 146 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
148 147 ex ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
149 148 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) → ( ∃ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
150 60 149 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } )
151 150 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } → 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )
152 57 151 impbid ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ↔ 𝑦 ∈ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
153 152 eqrdv ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } = ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
154 153 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
155 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
156 ssrab2 ⊢ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 )
157 156 a1i ⊢ ( 𝜑 → { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
158 155 157 ssfid ⊢ ( 𝜑 → { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ∈ Fin )
159 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → 𝐵 ∈ Fin )
160 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵
161 160 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ⊆ 𝐵 )
162 159 161 ssfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∈ Fin )
163 animorrl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑘 = 𝑖 ) → ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
164 inrab ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) }
165 164 a1i ⊢ ( ¬ 𝑘 = 𝑖 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) } )
166 rabn0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) )
167 166 biimpi ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) } ≠ ∅ → ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) )
168 eqtr2 ⊢ ( ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) → 𝑘 = 𝑖 )
169 168 adantl ⊢ ( ( ( ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) ) → 𝑘 = 𝑖 )
170 nfv ⊢ Ⅎ 𝑤 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 )
171 nfv ⊢ Ⅎ 𝑥 ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 )
172 fveqeq2 ⊢ ( 𝑥 = 𝑤 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ) )
173 fveqeq2 ⊢ ( 𝑥 = 𝑤 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) )
174 172 173 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) ↔ ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) ) )
175 170 171 174 cbvrexw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) ↔ ∃ 𝑤 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) )
176 175 biimpi ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) → ∃ 𝑤 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑤 ) = 𝑖 ) )
177 169 176 r19.29a ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) → 𝑘 = 𝑖 )
178 167 177 syl ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) } ≠ ∅ → 𝑘 = 𝑖 )
179 178 necon1bi ⊢ ( ¬ 𝑘 = 𝑖 → { 𝑥 ∈ 𝐵 ∣ ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) } = ∅ )
180 165 179 eqtrd ⊢ ( ¬ 𝑘 = 𝑖 → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ )
181 180 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ ¬ 𝑘 = 𝑖 ) → ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ )
182 181 olcd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ ¬ 𝑘 = 𝑖 ) → ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
183 163 182 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) ∧ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
184 183 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ) → ∀ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
185 184 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ∀ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
186 eqeq2 ⊢ ( 𝑘 = 𝑖 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 ) )
187 186 rabbidv ⊢ ( 𝑘 = 𝑖 → { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } = { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } )
188 187 disjor ⊢ ( Disj 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ↔ ∀ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ∀ 𝑖 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( 𝑘 = 𝑖 ∨ ( { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ∩ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑖 } ) = ∅ ) )
189 185 188 sylibr ⊢ ( 𝜑 → Disj 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } )
190 158 162 189 hashiun ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = Σ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) )
191 154 190 eqtr2d ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑚 ∈ ( 1 ... 𝑁 ) ∣ 𝑚 ∥ 𝑁 } ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = 𝑘 } ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑥 ) = ( 0g ‘ 𝐺 ) } ) )