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 biimpi ⊢ ( + Fn 𝐶 → + : 𝐶 ⟶ ran + )
8 7 adantr ⊢ ( ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) → + : 𝐶 ⟶ ran + )
9 8 3ad2ant3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → + : 𝐶 ⟶ ran + )
10 simpl3r ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 )
11 simp1l ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → 𝐹 Fn 𝐴 )
12 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
13 11 12 sylan ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
14 simp1r ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → 𝐺 Fn 𝐴 )
15 fnfvelrn ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
16 14 15 sylan ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑎 ) ∈ ran 𝐺 )
17 13 16 opelxpd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ ( ran 𝐹 × ran 𝐺 ) )
18 10 17 sseldd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) ∧ 𝑎 ∈ 𝐴 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ∈ 𝐶 )
19 9 18 cofmpt ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) )
20 df-ov ⊢ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) = ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ )
21 20 eqcomi ⊢ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) = ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) )
22 21 mpteq2i ⊢ ( 𝑎 ∈ 𝐴 ↦ ( + ‘ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) )
23 19 22 eqtrdi ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝑎 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐺 ‘ 𝑎 ) ⟩ ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
24 offval3 ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f + 𝐺 ) = ( 𝑎 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
25 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
26 fndm ⊢ ( 𝐺 Fn 𝐴 → dom 𝐺 = 𝐴 )
27 25 26 ineqan12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = ( 𝐴 ∩ 𝐴 ) )
28 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
29 27 28 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom 𝐹 ∩ dom 𝐺 ) = 𝐴 )
30 29 mpteq1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝑎 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
31 24 30 sylan9eqr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝐹 ∘f + 𝐺 ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) )
32 31 eqcomd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝐹 ∘f + 𝐺 ) )
33 32 3adant3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑎 ) + ( 𝐺 ‘ 𝑎 ) ) ) = ( 𝐹 ∘f + 𝐺 ) )
34 5 23 33 3eqtrd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( + Fn 𝐶 ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ 𝐶 ) ) → ( + ∘ ( 𝐻 ∘ 𝑆 ) ) = ( 𝐹 ∘f + 𝐺 ) )