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