Metamath Proof Explorer

Theorem offsplitfpar

Description: Express the function operation map oF by the functions defined in fsplit and fpar . (Contributed by AV, 4-Jan-2024)

Ref Expression
Hypotheses fsplitfpar.h ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
fsplitfpar.s ⊢ 𝑆 = ( ◡ ( 1st ↾ I ) ↾ 𝐴 )
Assertion offsplitfpar ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝐻 ∘ 𝑆 ) ) = ( 𝐹 ∘f + 𝐺 ) )

Proof

Step Hyp Ref Expression
1 fsplitfpar.h ⊢ 𝐻 = ( ( ◡ ( 1st ↾ ( V × V ) ) ∘ ( 𝐹 ∘ ( 1st ↾ ( V × V ) ) ) ) ∩ ( ◡ ( 2nd ↾ ( V × V ) ) ∘ ( 𝐺 ∘ ( 2nd ↾ ( V × V ) ) ) ) )
2 fsplitfpar.s ⊢ 𝑆 = ( ◡ ( 1st ↾ I ) ↾ 𝐴 )
3 1 2 fsplitfpar ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐻 ∘ 𝑆 ) = ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) )
4 3 coeq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( + ∘ ( 𝐻 ∘ 𝑆 ) ) = ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) )
5 4 3ad2ant1 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝐻 ∘ 𝑆 ) ) = ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) )
6 dffn3 ⊢ ( + Fn 𝐶 ↔ + : 𝐶 ⟶ ran + )
7 6 birani ⊢ ( ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) → + : 𝐶 ⟶ ran + )
8 7 3ad2ant3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → + : 𝐶 ⟶ ran + )
9 simpl3r ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 )
10 simp1l ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → 𝐹 Fn 𝐴 )
11 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
12 10 11 sylan ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
13 simp1r ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → 𝐺 Fn 𝐴 )
14 fnfvelrn ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
15 13 14 sylan ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
16 12 15 opelxpd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) )
17 9 16 sseldd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ 𝐶 )
18 8 17 cofmpt ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) )
19 df-ov ⊢ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) = ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
20 19 eqcomi ⊢ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) )
21 20 mpteq2i ⊢ ( 𝑎 ∈ 𝐴 ↦ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) )
22 18 21 eqtrdi ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
23 offval3 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f + 𝐺 ) = ( 𝑎 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
24 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
25 fndm ⊢ ( 𝐺 Fn 𝐴 → dom 𝐺 = 𝐴 )
26 24 25 ineqan12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐴 ) )
27 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
28 26 27 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = 𝐴 )
29 28 mpteq1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝑎 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
30 23 29 sylan9eqr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝐹 ∘f + 𝐺 ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
31 30 eqcomd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝐹 ∘f + 𝐺 ) )
32 31 3adant3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝐹 ∘f + 𝐺 ) )
33 5 22 32 3eqtrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝐻 ∘ 𝑆 ) ) = ( 𝐹 ∘f + 𝐺 ) )