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 = Base V
mhmimasplusg.c ⊢ C = Base W
mhmimasplusg.x ⊢ φ → X ∈ B
mhmimasplusg.y ⊢ φ → Y ∈ B
mhmimasplusg.1 ⊢ φ → F : B ⟶ onto C
mhmimasplusg.f ⊢ φ → F ∈ V MndHom W
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 = Base V
3 mhmimasplusg.c ⊢ C = Base W
4 mhmimasplusg.x ⊢ φ → X ∈ B
5 mhmimasplusg.y ⊢ φ → Y ∈ B
6 mhmimasplusg.1 ⊢ φ → F : B ⟶ onto C
7 mhmimasplusg.f ⊢ φ → F ∈ V MndHom W
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 ∈ V MndHom W
14 13 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ p ∈ B ∧ q ∈ B ∧ F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ∈ V MndHom W
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 ∈ V MndHom W ∧ 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 ∈ V MndHom W ∧ 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 = Base V
27 mhmrcl1 ⊢ F ∈ V MndHom W → 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