Metamath Proof Explorer

Theorem efmndmnd

Description: The monoid of endofunctions on a set A is actually a monoid. (Contributed by AV, 31-Jan-2024)

Ref Expression
Hypothesis ielefmnd.g ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
Assertion efmndmnd ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 ielefmnd.g ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 )
2 1 efmndsgrp ⊢ 𝐺 ∈ Smgrp
3 2 a1i ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Smgrp )
4 1 ielefmnd ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )
5 oveq1 ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) )
6 5 eqeq1d ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ↔ ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ) )
7 oveq2 ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) )
8 7 eqeq1d ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ↔ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) )
9 6 8 anbi12d ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ) ↔ ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) ) )
10 9 ralbidv ⊢ ( 𝑖 = ( I ↾ 𝐴 ) → ( ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ) ↔ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑖 = ( I ↾ 𝐴 ) ) → ( ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ) ↔ ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) ) )
12 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13 1 12 efmndbasf ⊢ ( 𝑓 ∈ ( Base ‘ 𝐺 ) → 𝑓 : 𝐴 ⟶ 𝐴 )
14 13 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → 𝑓 : 𝐴 ⟶ 𝐴 )
15 fcoi2 ⊢ ( 𝑓 : 𝐴 ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 )
16 fcoi1 ⊢ ( 𝑓 : 𝐴 ⟶ 𝐴 → ( 𝑓 ∘ ( I ↾ 𝐴 ) ) = 𝑓 )
17 15 16 jca ⊢ ( 𝑓 : 𝐴 ⟶ 𝐴 → ( ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ∧ ( 𝑓 ∘ ( I ↾ 𝐴 ) ) = 𝑓 ) )
18 14 17 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ∧ ( 𝑓 ∘ ( I ↾ 𝐴 ) ) = 𝑓 ) )
19 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
20 1 12 19 efmndov ⊢ ( ( ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = ( ( I ↾ 𝐴 ) ∘ 𝑓 ) )
21 4 20 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = ( ( I ↾ 𝐴 ) ∘ 𝑓 ) )
22 21 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ↔ ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ) )
23 4 anim1ci ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ) )
24 1 12 19 efmndov ⊢ ( ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = ( 𝑓 ∘ ( I ↾ 𝐴 ) ) )
25 23 24 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = ( 𝑓 ∘ ( I ↾ 𝐴 ) ) )
26 25 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ↔ ( 𝑓 ∘ ( I ↾ 𝐴 ) ) = 𝑓 ) )
27 22 26 anbi12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) ↔ ( ( ( I ↾ 𝐴 ) ∘ 𝑓 ) = 𝑓 ∧ ( 𝑓 ∘ ( I ↾ 𝐴 ) ) = 𝑓 ) ) )
28 18 27 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑓 ∈ ( Base ‘ 𝐺 ) ) → ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) )
29 28 ralrimiva ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) ( I ↾ 𝐴 ) ) = 𝑓 ) )
30 4 11 29 rspcedvd ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑖 ∈ ( Base ‘ 𝐺 ) ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ) )
31 12 19 ismnddef ⊢ ( 𝐺 ∈ Mnd ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑖 ∈ ( Base ‘ 𝐺 ) ∀ 𝑓 ∈ ( Base ‘ 𝐺 ) ( ( 𝑖 ( +g ‘ 𝐺 ) 𝑓 ) = 𝑓 ∧ ( 𝑓 ( +g ‘ 𝐺 ) 𝑖 ) = 𝑓 ) ) )
32 3 30 31 sylanbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd )