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	⊢ ( 𝜑 → 𝑄 ≃𝑚 𝐻 )