This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmicqusker

Description: The image H of a module homomorphism F is isomorphic with the quotient module Q over F 's kernel K . This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025)

Ref Expression
Hypotheses lmhmqusker.1 ⊢ 0 = ( 0g ‘ 𝐻 )
lmhmqusker.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) )
lmhmqusker.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
lmhmqusker.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
lmhmqusker.s ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
Assertion lmicqusker ( 𝜑 → 𝑄 ≃𝑚 𝐻 )

Proof

Step Hyp Ref Expression
1 lmhmqusker.1 ⊢ 0 = ( 0g ‘ 𝐻 )
2 lmhmqusker.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 LMHom 𝐻 ) )
3 lmhmqusker.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 lmhmqusker.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐾 ) )
5 lmhmqusker.s ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ 𝐻 ) )
6 imaeq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 “ 𝑝 ) = ( 𝐹 “ 𝑞 ) )
7 6 unieqd ⊢ ( 𝑝 = 𝑞 → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ 𝑞 ) )
8 7 cbvmptv ⊢ ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
9 1 2 3 4 5 8 lmhmqusker ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 LMIso 𝐻 ) )
10 brlmici ⊢ ( ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑝 ) ) ∈ ( 𝑄 LMIso 𝐻 ) → 𝑄 ≃𝑚 𝐻 )
11 9 10 syl ⊢ ( 𝜑 → 𝑄 ≃𝑚 𝐻 )