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 ˙ = 0 H
lmhmqusker.f ⊢ φ → F ∈ G LMHom H
lmhmqusker.k ⊢ K = F -1 0 ˙
lmhmqusker.q ⊢ Q = G / 𝑠 G ~ QG K
lmhmqusker.s ⊢ φ → ran ⁡ F = Base H
Assertion lmicqusker ⊢ φ → Q ≃ 𝑚 H

Proof

Step Hyp Ref Expression
1 lmhmqusker.1 ⊢ 0 ˙ = 0 H
2 lmhmqusker.f ⊢ φ → F ∈ G LMHom H
3 lmhmqusker.k ⊢ K = F -1 0 ˙
4 lmhmqusker.q ⊢ Q = G / 𝑠 G ~ QG K
5 lmhmqusker.s ⊢ φ → ran ⁡ F = Base H
6 imaeq2 ⊢ p = q → F p = F q
7 6 unieqd ⊢ p = q → ⋃ F p = ⋃ F q
8 7 cbvmptv ⊢ p ∈ Base Q ⟼ ⋃ F p = q ∈ Base Q ⟼ ⋃ F q
9 1 2 3 4 5 8 lmhmqusker ⊢ φ → p ∈ Base Q ⟼ ⋃ F p ∈ Q LMIso H
10 brlmici ⊢ p ∈ Base Q ⟼ ⋃ F p ∈ Q LMIso H → Q ≃ 𝑚 H
11 9 10 syl ⊢ φ → Q ≃ 𝑚 H