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 H = 1 st V × V -1 F 1 st V × V 2 nd V × V -1 G 2 nd V × V
fsplitfpar.s S = 1 st I -1 A
Assertion offsplitfpar F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ H S = F + ˙ f G

Proof

Step Hyp Ref Expression
1 fsplitfpar.h H = 1 st V × V -1 F 1 st V × V 2 nd V × V -1 G 2 nd V × V
2 fsplitfpar.s S = 1 st I -1 A
3 1 2 fsplitfpar F Fn A G Fn A H S = a A F a G a
4 3 coeq2d F Fn A G Fn A + ˙ H S = + ˙ a A F a G a
5 4 3ad2ant1 F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ H S = + ˙ a A F a G a
6 dffn3 + ˙ Fn C + ˙ : C ran + ˙
7 6 biimpi + ˙ Fn C + ˙ : C ran + ˙
8 7 adantr + ˙ Fn C ran F × ran G C + ˙ : C ran + ˙
9 8 3ad2ant3 F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ : C ran + ˙
10 simpl3r F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A ran F × ran G C
11 simp1l F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C F Fn A
12 fnfvelrn F Fn A a A F a ran F
13 11 12 sylan F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A F a ran F
14 simp1r F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C G Fn A
15 fnfvelrn G Fn A a A G a ran G
16 14 15 sylan F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A G a ran G
17 13 16 opelxpd F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A F a G a ran F × ran G
18 10 17 sseldd F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A F a G a C
19 9 18 cofmpt F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ a A F a G a = a A + ˙ F a G a
20 df-ov F a + ˙ G a = + ˙ F a G a
21 20 eqcomi + ˙ F a G a = F a + ˙ G a
22 21 mpteq2i a A + ˙ F a G a = a A F a + ˙ G a
23 19 22 eqtrdi F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ a A F a G a = a A F a + ˙ G a
24 offval3 F V G W F + ˙ f G = a dom F dom G F a + ˙ G a
25 fndm F Fn A dom F = A
26 fndm G Fn A dom G = A
27 25 26 ineqan12d F Fn A G Fn A dom F dom G = A A
28 inidm A A = A
29 27 28 eqtrdi F Fn A G Fn A dom F dom G = A
30 29 mpteq1d F Fn A G Fn A a dom F dom G F a + ˙ G a = a A F a + ˙ G a
31 24 30 sylan9eqr F Fn A G Fn A F V G W F + ˙ f G = a A F a + ˙ G a
32 31 eqcomd F Fn A G Fn A F V G W a A F a + ˙ G a = F + ˙ f G
33 32 3adant3 F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C a A F a + ˙ G a = F + ˙ f G
34 5 23 33 3eqtrd F Fn A G Fn A F V G W + ˙ Fn C ran F × ran G C + ˙ H S = F + ˙ f G