Metamath Proof Explorer

Theorem mndpfo

Description: The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 11-Oct-2013) (Revised by AV, 23-Jan-2020)

Ref Expression
Hypotheses mndpf.b âŠĒ ðĩ = ( Base ‘ 𝐚 )
mndpf.p âŠĒ âĻĢ = ( +𝑓 ‘ 𝐚 )
Assertion mndpfo ( 𝐚 ∈ Mnd → âĻĢ : ( ðĩ × ðĩ ) –onto→ ðĩ )

Proof

Step Hyp Ref Expression
1 mndpf.b âŠĒ ðĩ = ( Base ‘ 𝐚 )
2 mndpf.p âŠĒ âĻĢ = ( +𝑓 ‘ 𝐚 )
3 1 2 mndplusf âŠĒ ( 𝐚 ∈ Mnd → âĻĢ : ( ðĩ × ðĩ ) âŸķ ðĩ )
4 simpr âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ð‘Ĩ ∈ ðĩ )
5 eqid âŠĒ ( 0g ‘ 𝐚 ) = ( 0g ‘ 𝐚 )
6 1 5 mndidcl âŠĒ ( 𝐚 ∈ Mnd → ( 0g ‘ 𝐚 ) ∈ ðĩ )
7 6 adantr âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ( 0g ‘ 𝐚 ) ∈ ðĩ )
8 eqid âŠĒ ( +g ‘ 𝐚 ) = ( +g ‘ 𝐚 )
9 1 8 5 mndrid âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ( ð‘Ĩ ( +g ‘ 𝐚 ) ( 0g ‘ 𝐚 ) ) = ð‘Ĩ )
10 9 eqcomd âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ð‘Ĩ = ( ð‘Ĩ ( +g ‘ 𝐚 ) ( 0g ‘ 𝐚 ) ) )
11 rspceov âŠĒ ( ( ð‘Ĩ ∈ ðĩ ∧ ( 0g ‘ 𝐚 ) ∈ ðĩ ∧ ð‘Ĩ = ( ð‘Ĩ ( +g ‘ 𝐚 ) ( 0g ‘ 𝐚 ) ) ) → ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ ( +g ‘ 𝐚 ) 𝑧 ) )
12 4 7 10 11 syl3anc âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ ( +g ‘ 𝐚 ) 𝑧 ) )
13 1 8 2 plusfval âŠĒ ( ( ð‘Ķ ∈ ðĩ ∧ 𝑧 ∈ ðĩ ) → ( ð‘Ķ âĻĢ 𝑧 ) = ( ð‘Ķ ( +g ‘ 𝐚 ) 𝑧 ) )
14 13 eqeq2d âŠĒ ( ( ð‘Ķ ∈ ðĩ ∧ 𝑧 ∈ ðĩ ) → ( ð‘Ĩ = ( ð‘Ķ âĻĢ 𝑧 ) ↔ ð‘Ĩ = ( ð‘Ķ ( +g ‘ 𝐚 ) 𝑧 ) ) )
15 14 2rexbiia âŠĒ ( ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ âĻĢ 𝑧 ) ↔ ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ ( +g ‘ 𝐚 ) 𝑧 ) )
16 12 15 sylibr âŠĒ ( ( 𝐚 ∈ Mnd ∧ ð‘Ĩ ∈ ðĩ ) → ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ âĻĢ 𝑧 ) )
17 16 ralrimiva âŠĒ ( 𝐚 ∈ Mnd → ∀ ð‘Ĩ ∈ ðĩ ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ âĻĢ 𝑧 ) )
18 foov âŠĒ ( âĻĢ : ( ðĩ × ðĩ ) –onto→ ðĩ ↔ ( âĻĢ : ( ðĩ × ðĩ ) âŸķ ðĩ ∧ ∀ ð‘Ĩ ∈ ðĩ ∃ ð‘Ķ ∈ ðĩ ∃ 𝑧 ∈ ðĩ ð‘Ĩ = ( ð‘Ķ âĻĢ 𝑧 ) ) )
19 3 17 18 sylanbrc âŠĒ ( 𝐚 ∈ Mnd → âĻĢ : ( ðĩ × ðĩ ) –onto→ ðĩ )