Metamath Proof Explorer

Theorem xpcan2

Description: Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011)

Ref Expression
Assertion xpcan2 
|- ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 xp11 
 |-  ( ( A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> ( A = B /\ C = C ) ) )
2 eqid 
 |-  C = C
3 2 biantru 
 |-  ( A = B <-> ( A = B /\ C = C ) )
4 1 3 bitr4di 
 |-  ( ( A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
5 nne 
 |-  ( -. A =/= (/) <-> A = (/) )
6 simpl 
 |-  ( ( A = (/) /\ C =/= (/) ) -> A = (/) )
7 xpeq1 
 |-  ( A = (/) -> ( A X. C ) = ( (/) X. C ) )
8 0xp 
 |-  ( (/) X. C ) = (/)
9 7 8 eqtrdi 
 |-  ( A = (/) -> ( A X. C ) = (/) )
10 9 eqeq1d 
 |-  ( A = (/) -> ( ( A X. C ) = ( B X. C ) <-> (/) = ( B X. C ) ) )
11 eqcom 
 |-  ( (/) = ( B X. C ) <-> ( B X. C ) = (/) )
12 10 11 bitrdi 
 |-  ( A = (/) -> ( ( A X. C ) = ( B X. C ) <-> ( B X. C ) = (/) ) )
13 12 adantr 
 |-  ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> ( B X. C ) = (/) ) )
14 df-ne 
 |-  ( C =/= (/) <-> -. C = (/) )
15 xpeq0 
 |-  ( ( B X. C ) = (/) <-> ( B = (/) \/ C = (/) ) )
16 orel2 
 |-  ( -. C = (/) -> ( ( B = (/) \/ C = (/) ) -> B = (/) ) )
17 15 16 syl5bi 
 |-  ( -. C = (/) -> ( ( B X. C ) = (/) -> B = (/) ) )
18 14 17 sylbi 
 |-  ( C =/= (/) -> ( ( B X. C ) = (/) -> B = (/) ) )
19 18 adantl 
 |-  ( ( A = (/) /\ C =/= (/) ) -> ( ( B X. C ) = (/) -> B = (/) ) )
20 13 19 sylbid 
 |-  ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) -> B = (/) ) )
21 eqtr3 
 |-  ( ( A = (/) /\ B = (/) ) -> A = B )
22 6 20 21 syl6an 
 |-  ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) -> A = B ) )
23 xpeq1 
 |-  ( A = B -> ( A X. C ) = ( B X. C ) )
24 22 23 impbid1 
 |-  ( ( A = (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
25 5 24 sylanb 
 |-  ( ( -. A =/= (/) /\ C =/= (/) ) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )
26 4 25 pm2.61ian 
 |-  ( C =/= (/) -> ( ( A X. C ) = ( B X. C ) <-> A = B ) )