Metamath Proof Explorer

Theorem xpima

Description: Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Assertion xpima 
|- ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B )

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( ( A i^i C ) = (/) \/ -. ( A i^i C ) = (/) )
2 df-ima 
 |-  ( ( A X. B ) " C ) = ran ( ( A X. B ) |` C )
3 df-res 
 |-  ( ( A X. B ) |` C ) = ( ( A X. B ) i^i ( C X. _V ) )
4 3 rneqi 
 |-  ran ( ( A X. B ) |` C ) = ran ( ( A X. B ) i^i ( C X. _V ) )
5 2 4 eqtri 
 |-  ( ( A X. B ) " C ) = ran ( ( A X. B ) i^i ( C X. _V ) )
6 inxp 
 |-  ( ( A X. B ) i^i ( C X. _V ) ) = ( ( A i^i C ) X. ( B i^i _V ) )
7 6 rneqi 
 |-  ran ( ( A X. B ) i^i ( C X. _V ) ) = ran ( ( A i^i C ) X. ( B i^i _V ) )
8 inv1 
 |-  ( B i^i _V ) = B
9 8 xpeq2i 
 |-  ( ( A i^i C ) X. ( B i^i _V ) ) = ( ( A i^i C ) X. B )
10 9 rneqi 
 |-  ran ( ( A i^i C ) X. ( B i^i _V ) ) = ran ( ( A i^i C ) X. B )
11 5 7 10 3eqtri 
 |-  ( ( A X. B ) " C ) = ran ( ( A i^i C ) X. B )
12 xpeq1 
 |-  ( ( A i^i C ) = (/) -> ( ( A i^i C ) X. B ) = ( (/) X. B ) )
13 0xp 
 |-  ( (/) X. B ) = (/)
14 12 13 eqtrdi 
 |-  ( ( A i^i C ) = (/) -> ( ( A i^i C ) X. B ) = (/) )
15 14 rneqd 
 |-  ( ( A i^i C ) = (/) -> ran ( ( A i^i C ) X. B ) = ran (/) )
16 rn0 
 |-  ran (/) = (/)
17 15 16 eqtrdi 
 |-  ( ( A i^i C ) = (/) -> ran ( ( A i^i C ) X. B ) = (/) )
18 11 17 syl5eq 
 |-  ( ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = (/) )
19 18 ancli 
 |-  ( ( A i^i C ) = (/) -> ( ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = (/) ) )
20 df-ne 
 |-  ( ( A i^i C ) =/= (/) <-> -. ( A i^i C ) = (/) )
21 rnxp 
 |-  ( ( A i^i C ) =/= (/) -> ran ( ( A i^i C ) X. B ) = B )
22 20 21 sylbir 
 |-  ( -. ( A i^i C ) = (/) -> ran ( ( A i^i C ) X. B ) = B )
23 11 22 syl5eq 
 |-  ( -. ( A i^i C ) = (/) -> ( ( A X. B ) " C ) = B )
24 23 ancli 
 |-  ( -. ( A i^i C ) = (/) -> ( -. ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = B ) )
25 19 24 orim12i 
 |-  ( ( ( A i^i C ) = (/) \/ -. ( A i^i C ) = (/) ) -> ( ( ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = (/) ) \/ ( -. ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = B ) ) )
26 1 25 ax-mp 
 |-  ( ( ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = (/) ) \/ ( -. ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = B ) )
27 eqif 
 |-  ( ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B ) <-> ( ( ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = (/) ) \/ ( -. ( A i^i C ) = (/) /\ ( ( A X. B ) " C ) = B ) ) )
28 26 27 mpbir 
 |-  ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B )