Metamath Proof Explorer

Theorem mhmimasplusg

Description: Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses mhmimasplusg.w ⊢ 𝑊 = ( 𝐹 “s 𝑉 )
mhmimasplusg.b ⊢ 𝐵 = ( Base ‘ 𝑉 )
mhmimasplusg.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
mhmimasplusg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mhmimasplusg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
mhmimasplusg.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ 𝐶 )
mhmimasplusg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) )
mhmimasplusg.2 ⊢ + = ( +g ‘ 𝑉 )
mhmimasplusg.3 ⊢ ⨣ = ( +g ‘ 𝑊 )
Assertion mhmimasplusg ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mhmimasplusg.w ⊢ 𝑊 = ( 𝐹 “s 𝑉 )
2 mhmimasplusg.b ⊢ 𝐵 = ( Base ‘ 𝑉 )
3 mhmimasplusg.c ⊢ 𝐶 = ( Base ‘ 𝑊 )
4 mhmimasplusg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 mhmimasplusg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 mhmimasplusg.1 ⊢ ( 𝜑 → 𝐹 : 𝐵 –onto→ 𝐶 )
7 mhmimasplusg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) )
8 mhmimasplusg.2 ⊢ + = ( +g ‘ 𝑉 )
9 mhmimasplusg.3 ⊢ ⨣ = ( +g ‘ 𝑊 )
10 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) )
11 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) )
12 10 11 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑝 ) ⨣ ( 𝐹 ‘ 𝑞 ) ) )
13 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) )
14 13 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) )
15 simpl2l ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → 𝑎 ∈ 𝐵 )
16 simpl2r ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → 𝑏 ∈ 𝐵 )
17 2 8 9 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) )
19 simpl3l ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → 𝑝 ∈ 𝐵 )
20 simpl3r ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → 𝑞 ∈ 𝐵 )
21 2 8 9 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) = ( ( 𝐹 ‘ 𝑝 ) ⨣ ( 𝐹 ‘ 𝑞 ) ) )
22 14 19 20 21 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) = ( ( 𝐹 ‘ 𝑝 ) ⨣ ( 𝐹 ‘ 𝑞 ) ) )
23 12 18 22 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) )
24 23 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
25 1 a1i ⊢ ( 𝜑 → 𝑊 = ( 𝐹 “s 𝑉 ) )
26 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑉 ) )
27 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑉 MndHom 𝑊 ) → 𝑉 ∈ Mnd )
28 7 27 syl ⊢ ( 𝜑 → 𝑉 ∈ Mnd )
29 6 24 25 26 28 8 9 imasaddval ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) )
30 4 5 29 mpd3an23 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ⨣ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑌 ) ) )