Metamath Proof Explorer

Theorem smndex1mgm

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a magma. (Contributed by AV, 14-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion smndex1mgm 𝑆 ∈ Mgm

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6 smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7 1 2 3 4 5 smndex1basss ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
8 ssel ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( 𝑎 ∈ 𝐵 → 𝑎 ∈ ( Base ‘ 𝑀 ) ) )
9 ssel ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( Base ‘ 𝑀 ) ) )
10 8 9 anim12d ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) ) )
11 7 10 ax-mp ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) )
12 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
13 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
14 1 12 13 efmndov ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ∘ 𝑏 ) )
15 11 14 syl ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) = ( 𝑎 ∘ 𝑏 ) )
16 simpl ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐼 ) → 𝑎 = 𝐼 )
17 simpr ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐼 ) → 𝑏 = 𝐼 )
18 16 17 coeq12d ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐼 ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐼 ∘ 𝐼 ) )
19 1 2 3 smndex1iidm ⊢ ( 𝐼 ∘ 𝐼 ) = 𝐼
20 18 19 eqtrdi ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐼 ) → ( 𝑎 ∘ 𝑏 ) = 𝐼 )
21 20 orcd ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑏 = 𝐼 ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
22 21 ex ⊢ ( 𝑎 = 𝐼 → ( 𝑏 = 𝐼 → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
23 simpll ⊢ ( ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → 𝑎 = 𝐼 )
24 simpr ⊢ ( ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → 𝑏 = ( 𝐺 ‘ 𝑘 ) )
25 23 24 coeq12d ⊢ ( ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) )
26 1 2 3 4 smndex1igid ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
27 26 ad2antlr ⊢ ( ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
28 25 27 eqtrd ⊢ ( ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
29 28 ex ⊢ ( ( 𝑎 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑏 = ( 𝐺 ‘ 𝑘 ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
30 29 reximdva ⊢ ( 𝑎 = 𝐼 → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
31 30 imp ⊢ ( ( 𝑎 = 𝐼 ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
32 31 olcd ⊢ ( ( 𝑎 = 𝐼 ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
33 32 ex ⊢ ( 𝑎 = 𝐼 → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
34 22 33 jaod ⊢ ( 𝑎 = 𝐼 → ( ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
35 simpr ⊢ ( ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → 𝑎 = ( 𝐺 ‘ 𝑘 ) )
36 simpll ⊢ ( ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → 𝑏 = 𝐼 )
37 35 36 coeq12d ⊢ ( ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) )
38 1 2 3 smndex1ibas ⊢ 𝐼 ∈ ( Base ‘ 𝑀 )
39 1 2 3 4 smndex1gid ⊢ ( ( 𝐼 ∈ ( Base ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) )
40 38 39 mpan ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) )
41 40 ad2antlr ⊢ ( ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) )
42 37 41 eqtrd ⊢ ( ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
43 42 ex ⊢ ( ( 𝑏 = 𝐼 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
44 43 reximdva ⊢ ( 𝑏 = 𝐼 → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
45 44 imp ⊢ ( ( 𝑏 = 𝐼 ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
46 45 olcd ⊢ ( ( 𝑏 = 𝐼 ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
47 46 expcom ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( 𝑏 = 𝐼 → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
48 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑚 ) )
49 48 eqeq2d ⊢ ( 𝑘 = 𝑚 → ( 𝑏 = ( 𝐺 ‘ 𝑘 ) ↔ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ↔ ∃ 𝑚 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑚 ) )
51 simpr ⊢ ( ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → 𝑎 = ( 𝐺 ‘ 𝑘 ) )
52 simpllr ⊢ ( ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → 𝑏 = ( 𝐺 ‘ 𝑚 ) )
53 51 52 coeq12d ⊢ ( ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( ( 𝐺 ‘ 𝑘 ) ∘ ( 𝐺 ‘ 𝑚 ) ) )
54 1 2 3 4 smndex1gbas ⊢ ( 𝑚 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝑚 ) ∈ ( Base ‘ 𝑀 ) )
55 1 2 3 4 smndex1gid ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ∈ ( Base ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ ( 𝐺 ‘ 𝑚 ) ) = ( 𝐺 ‘ 𝑘 ) )
56 54 55 sylan ⊢ ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ ( 𝐺 ‘ 𝑚 ) ) = ( 𝐺 ‘ 𝑘 ) )
57 56 ad4ant13 ⊢ ( ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ ( 𝐺 ‘ 𝑚 ) ) = ( 𝐺 ‘ 𝑘 ) )
58 53 57 eqtrd ⊢ ( ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
59 58 ex ⊢ ( ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
60 59 reximdva ⊢ ( ( 𝑚 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑏 = ( 𝐺 ‘ 𝑚 ) ) → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
61 60 rexlimiva ⊢ ( ∃ 𝑚 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑚 ) → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
62 61 imp ⊢ ( ( ∃ 𝑚 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑚 ) ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
63 62 olcd ⊢ ( ( ∃ 𝑚 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑚 ) ∧ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
64 63 expcom ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( ∃ 𝑚 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑚 ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
65 50 64 syl5bi ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
66 47 65 jaod ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
67 34 66 jaoi ⊢ ( ( 𝑎 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
68 67 imp ⊢ ( ( ( 𝑎 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) ∧ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) ) → ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
69 5 eleq2i ⊢ ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
70 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
71 70 sneqd ⊢ ( 𝑛 = 𝑘 → { ( 𝐺 ‘ 𝑛 ) } = { ( 𝐺 ‘ 𝑘 ) } )
72 71 cbviunv ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } = ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) }
73 72 uneq2i ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) = ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } )
74 73 eleq2i ⊢ ( 𝑎 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ 𝑎 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
75 69 74 bitri ⊢ ( 𝑎 ∈ 𝐵 ↔ 𝑎 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
76 elun ⊢ ( 𝑎 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑎 ∈ { 𝐼 } ∨ 𝑎 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
77 velsn ⊢ ( 𝑎 ∈ { 𝐼 } ↔ 𝑎 = 𝐼 )
78 eliun ⊢ ( 𝑎 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 ∈ { ( 𝐺 ‘ 𝑘 ) } )
79 velsn ⊢ ( 𝑎 ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ 𝑎 = ( 𝐺 ‘ 𝑘 ) )
80 79 rexbii ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) )
81 78 80 bitri ⊢ ( 𝑎 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) )
82 77 81 orbi12i ⊢ ( ( 𝑎 ∈ { 𝐼 } ∨ 𝑎 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑎 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) )
83 75 76 82 3bitri ⊢ ( 𝑎 ∈ 𝐵 ↔ ( 𝑎 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) )
84 5 eleq2i ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
85 73 eleq2i ⊢ ( 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
86 84 85 bitri ⊢ ( 𝑏 ∈ 𝐵 ↔ 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
87 elun ⊢ ( 𝑏 ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑏 ∈ { 𝐼 } ∨ 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
88 velsn ⊢ ( 𝑏 ∈ { 𝐼 } ↔ 𝑏 = 𝐼 )
89 eliun ⊢ ( 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } )
90 velsn ⊢ ( 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ 𝑏 = ( 𝐺 ‘ 𝑘 ) )
91 90 rexbii ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) )
92 89 91 bitri ⊢ ( 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) )
93 88 92 orbi12i ⊢ ( ( 𝑏 ∈ { 𝐼 } ∨ 𝑏 ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) )
94 86 87 93 3bitri ⊢ ( 𝑏 ∈ 𝐵 ↔ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) )
95 83 94 anbi12i ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ↔ ( ( 𝑎 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑎 = ( 𝐺 ‘ 𝑘 ) ) ∧ ( 𝑏 = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑏 = ( 𝐺 ‘ 𝑘 ) ) ) )
96 5 eleq2i ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ 𝐵 ↔ ( 𝑎 ∘ 𝑏 ) ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
97 73 eleq2i ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ ( 𝑎 ∘ 𝑏 ) ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
98 96 97 bitri ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ 𝐵 ↔ ( 𝑎 ∘ 𝑏 ) ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
99 elun ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ ( { 𝐼 } ∪ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( ( 𝑎 ∘ 𝑏 ) ∈ { 𝐼 } ∨ ( 𝑎 ∘ 𝑏 ) ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) )
100 vex ⊢ 𝑎 ∈ V
101 vex ⊢ 𝑏 ∈ V
102 100 101 coex ⊢ ( 𝑎 ∘ 𝑏 ) ∈ V
103 102 elsn ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ { 𝐼 } ↔ ( 𝑎 ∘ 𝑏 ) = 𝐼 )
104 eliun ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) ∈ { ( 𝐺 ‘ 𝑘 ) } )
105 102 elsn ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
106 105 rexbii ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) ∈ { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
107 104 106 bitri ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) )
108 103 107 orbi12i ⊢ ( ( ( 𝑎 ∘ 𝑏 ) ∈ { 𝐼 } ∨ ( 𝑎 ∘ 𝑏 ) ∈ ∪ 𝑘 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑘 ) } ) ↔ ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
109 98 99 108 3bitri ⊢ ( ( 𝑎 ∘ 𝑏 ) ∈ 𝐵 ↔ ( ( 𝑎 ∘ 𝑏 ) = 𝐼 ∨ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝑎 ∘ 𝑏 ) = ( 𝐺 ‘ 𝑘 ) ) )
110 68 95 109 3imtr4i ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∘ 𝑏 ) ∈ 𝐵 )
111 15 110 eqeltrd ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
112 111 rgen2 ⊢ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵
113 6 ovexi ⊢ 𝑆 ∈ V
114 1 2 3 4 5 6 smndex1bas ⊢ ( Base ‘ 𝑆 ) = 𝐵
115 114 eqcomi ⊢ 𝐵 = ( Base ‘ 𝑆 )
116 115 fvexi ⊢ 𝐵 ∈ V
117 6 13 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
118 116 117 ax-mp ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 )
119 115 118 ismgm ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 ) )
120 113 119 ax-mp ⊢ ( 𝑆 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) ∈ 𝐵 )
121 112 120 mpbir ⊢ 𝑆 ∈ Mgm