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 
|- W = ( F "s V )
mhmimasplusg.b 
|- B = ( Base ` V )
mhmimasplusg.c 
|- C = ( Base ` W )
mhmimasplusg.x 
|- ( ph -> X e. B )
mhmimasplusg.y 
|- ( ph -> Y e. B )
mhmimasplusg.1 
|- ( ph -> F : B -onto-> C )
mhmimasplusg.f 
|- ( ph -> F e. ( V MndHom W ) )
mhmimasplusg.2 
|- .+ = ( +g ` V )
mhmimasplusg.3 
|- .+^ = ( +g ` W )
Assertion mhmimasplusg 
|- ( ph -> ( ( F ` X ) .+^ ( F ` Y ) ) = ( F ` ( X .+ Y ) ) )

Proof

Step Hyp Ref Expression
1 mhmimasplusg.w 
 |-  W = ( F "s V )
2 mhmimasplusg.b 
 |-  B = ( Base ` V )
3 mhmimasplusg.c 
 |-  C = ( Base ` W )
4 mhmimasplusg.x 
 |-  ( ph -> X e. B )
5 mhmimasplusg.y 
 |-  ( ph -> Y e. B )
6 mhmimasplusg.1 
 |-  ( ph -> F : B -onto-> C )
7 mhmimasplusg.f 
 |-  ( ph -> F e. ( V MndHom W ) )
8 mhmimasplusg.2 
 |-  .+ = ( +g ` V )
9 mhmimasplusg.3 
 |-  .+^ = ( +g ` W )
10 simprl 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( F ` a ) = ( F ` p ) )
11 simprr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( F ` b ) = ( F ` q ) )
12 10 11 oveq12d 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( ( F ` a ) .+^ ( F ` b ) ) = ( ( F ` p ) .+^ ( F ` q ) ) )
13 7 3ad2ant1 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> F e. ( V MndHom W ) )
14 13 adantr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> F e. ( V MndHom W ) )
15 simpl2l 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> a e. B )
16 simpl2r 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> b e. B )
17 2 8 9 mhmlin 
 |-  ( ( F e. ( V MndHom W ) /\ a e. B /\ b e. B ) -> ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) )
19 simpl3l 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> p e. B )
20 simpl3r 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> q e. B )
21 2 8 9 mhmlin 
 |-  ( ( F e. ( V MndHom W ) /\ p e. B /\ q e. B ) -> ( F ` ( p .+ q ) ) = ( ( F ` p ) .+^ ( F ` q ) ) )
22 14 19 20 21 syl3anc 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( F ` ( p .+ q ) ) = ( ( F ` p ) .+^ ( F ` q ) ) )
23 12 18 22 3eqtr4d 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) /\ ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) )
24 23 ex 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ ( p e. B /\ q e. B ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
25 1 a1i 
 |-  ( ph -> W = ( F "s V ) )
26 2 a1i 
 |-  ( ph -> B = ( Base ` V ) )
27 mhmrcl1 
 |-  ( F e. ( V MndHom W ) -> V e. Mnd )
28 7 27 syl 
 |-  ( ph -> V e. Mnd )
29 6 24 25 26 28 8 9 imasaddval 
 |-  ( ( ph /\ X e. B /\ Y e. B ) -> ( ( F ` X ) .+^ ( F ` Y ) ) = ( F ` ( X .+ Y ) ) )
30 4 5 29 mpd3an23 
 |-  ( ph -> ( ( F ` X ) .+^ ( F ` Y ) ) = ( F ` ( X .+ Y ) ) )