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“𝑠V
mhmimasplusg.b ⊢B=BaseV
mhmimasplusg.c ⊢C=BaseW
mhmimasplusg.x ⊢φ→X∈B
mhmimasplusg.y ⊢φ→Y∈B
mhmimasplusg.1 ⊢φ→F:B⟶ontoC
mhmimasplusg.f ⊢φ→F∈VMndHomW
mhmimasplusg.2 ⊢+˙=+V
mhmimasplusg.3 ⊢⨣˙=+W
Assertion mhmimasplusg ⊢φ→F⁡X⨣˙F⁡Y=F⁡X+˙Y

Proof

Step Hyp Ref Expression
1 mhmimasplusg.w ⊢W=F“𝑠V
2 mhmimasplusg.b ⊢B=BaseV
3 mhmimasplusg.c ⊢C=BaseW
4 mhmimasplusg.x ⊢φ→X∈B
5 mhmimasplusg.y ⊢φ→Y∈B
6 mhmimasplusg.1 ⊢φ→F:B⟶ontoC
7 mhmimasplusg.f ⊢φ→F∈VMndHomW
8 mhmimasplusg.2 ⊢+˙=+V
9 mhmimasplusg.3 ⊢⨣˙=+W
10 simprl ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡a=F⁡p
11 simprr ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡b=F⁡q
12 10 11 oveq12d ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡a⨣˙F⁡b=F⁡p⨣˙F⁡q
13 7 3ad2ant1 ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B→F∈VMndHomW
14 13 adantr ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F∈VMndHomW
15 simpl2l ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→a∈B
16 simpl2r ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→b∈B
17 2 8 9 mhmlin ⊢F∈VMndHomW∧a∈B∧b∈B→F⁡a+˙b=F⁡a⨣˙F⁡b
18 14 15 16 17 syl3anc ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡a+˙b=F⁡a⨣˙F⁡b
19 simpl3l ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→p∈B
20 simpl3r ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→q∈B
21 2 8 9 mhmlin ⊢F∈VMndHomW∧p∈B∧q∈B→F⁡p+˙q=F⁡p⨣˙F⁡q
22 14 19 20 21 syl3anc ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡p+˙q=F⁡p⨣˙F⁡q
23 12 18 22 3eqtr4d ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B∧F⁡a=F⁡p∧F⁡b=F⁡q→F⁡a+˙b=F⁡p+˙q
24 23 ex ⊢φ∧a∈B∧b∈B∧p∈B∧q∈B→F⁡a=F⁡p∧F⁡b=F⁡q→F⁡a+˙b=F⁡p+˙q
25 1 a1i ⊢φ→W=F“𝑠V
26 2 a1i ⊢φ→B=BaseV
27 mhmrcl1 ⊢F∈VMndHomW→V∈Mnd
28 7 27 syl ⊢φ→V∈Mnd
29 6 24 25 26 28 8 9 imasaddval ⊢φ∧X∈B∧Y∈B→F⁡X⨣˙F⁡Y=F⁡X+˙Y
30 4 5 29 mpd3an23 ⊢φ→F⁡X⨣˙F⁡Y=F⁡X+˙Y