Metamath Proof Explorer

Theorem tfsconcat00

Description: The concatentation of two empty series results in an empty series. (Contributed by RP, 25-Feb-2025)

Ref

Expression

Hypothesis

tfsconcat.op

|- .+ = ( a e. _V , b e. _V |-> ( a u. { <. x , y >. | ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )

Assertion

|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A = (/) /\ B = (/) ) <-> ( A .+ B ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	\|- .+ = ( a e. _V , b e. _V \|-> ( a u. { <. x , y >. \| ( x e. ( ( dom a +o dom b ) \ dom a ) /\ E. z e. dom b ( x = ( dom a +o z ) /\ y = ( b ` z ) ) ) } ) )
2	1	tfsconcatrn	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ran ( A .+ B ) = ( ran A u. ran B ) )
3	2	eqeq1d	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ran ( A .+ B ) = (/) <-> ( ran A u. ran B ) = (/) ) )
4	1	tfsconcatfn	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( A .+ B ) Fn ( C +o D ) )
5		fnrel	\|- ( ( A .+ B ) Fn ( C +o D ) -> Rel ( A .+ B ) )
6		relrn0	\|- ( Rel ( A .+ B ) -> ( ( A .+ B ) = (/) <-> ran ( A .+ B ) = (/) ) )
7	4 5 6	3syl	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A .+ B ) = (/) <-> ran ( A .+ B ) = (/) ) )
8		fnrel	\|- ( A Fn C -> Rel A )
9		relrn0	\|- ( Rel A -> ( A = (/) <-> ran A = (/) ) )
10	8 9	syl	\|- ( A Fn C -> ( A = (/) <-> ran A = (/) ) )
11		fnrel	\|- ( B Fn D -> Rel B )
12		relrn0	\|- ( Rel B -> ( B = (/) <-> ran B = (/) ) )
13	11 12	syl	\|- ( B Fn D -> ( B = (/) <-> ran B = (/) ) )
14	10 13	bi2anan9	\|- ( ( A Fn C /\ B Fn D ) -> ( ( A = (/) /\ B = (/) ) <-> ( ran A = (/) /\ ran B = (/) ) ) )
15		un00	\|- ( ( ran A = (/) /\ ran B = (/) ) <-> ( ran A u. ran B ) = (/) )
16	14 15	bitrdi	\|- ( ( A Fn C /\ B Fn D ) -> ( ( A = (/) /\ B = (/) ) <-> ( ran A u. ran B ) = (/) ) )
17	16	adantr	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A = (/) /\ B = (/) ) <-> ( ran A u. ran B ) = (/) ) )
18	3 7 17	3bitr4rd	\|- ( ( ( A Fn C /\ B Fn D ) /\ ( C e. On /\ D e. On ) ) -> ( ( A = (/) /\ B = (/) ) <-> ( A .+ B ) = (/) ) )