Description: The value of the group operation of the monoid of endofunctions on A . (Contributed by AV, 27-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | efmndtset.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
efmndplusg.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | ||
efmndplusg.p | ⊢ + = ( +g ‘ 𝐺 ) | ||
Assertion | efmndov | ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efmndtset.g | ⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) | |
2 | efmndplusg.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
3 | efmndplusg.p | ⊢ + = ( +g ‘ 𝐺 ) | |
4 | coexg | ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∘ 𝑌 ) ∈ V ) | |
5 | coeq1 | ⊢ ( 𝑓 = 𝑋 → ( 𝑓 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑔 ) ) | |
6 | coeq2 | ⊢ ( 𝑔 = 𝑌 → ( 𝑋 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑌 ) ) | |
7 | 1 2 3 | efmndplusg | ⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) ) |
8 | 5 6 7 | ovmpog | ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∘ 𝑌 ) ∈ V ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) ) |
9 | 4 8 | mpd3an3 | ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) ) |