Metamath Proof Explorer

Theorem xpcan

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

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

Proof

Step Hyp Ref Expression
1 xp11 
 |-  ( ( C =/= (/) /\ A =/= (/) ) -> ( ( C X. A ) = ( C X. B ) <-> ( C = C /\ A = B ) ) )
2 eqid 
 |-  C = C
3 2 biantrur 
 |-  ( A = B <-> ( C = C /\ A = B ) )
4 1 3 bitr4di 
 |-  ( ( C =/= (/) /\ A =/= (/) ) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
5 nne 
 |-  ( -. A =/= (/) <-> A = (/) )
6 simpr 
 |-  ( ( C =/= (/) /\ A = (/) ) -> A = (/) )
7 xpeq2 
 |-  ( A = (/) -> ( C X. A ) = ( C X. (/) ) )
8 xp0 
 |-  ( C X. (/) ) = (/)
9 7 8 eqtrdi 
 |-  ( A = (/) -> ( C X. A ) = (/) )
10 9 eqeq1d 
 |-  ( A = (/) -> ( ( C X. A ) = ( C X. B ) <-> (/) = ( C X. B ) ) )
11 eqcom 
 |-  ( (/) = ( C X. B ) <-> ( C X. B ) = (/) )
12 10 11 bitrdi 
 |-  ( A = (/) -> ( ( C X. A ) = ( C X. B ) <-> ( C X. B ) = (/) ) )
13 12 adantl 
 |-  ( ( C =/= (/) /\ A = (/) ) -> ( ( C X. A ) = ( C X. B ) <-> ( C X. B ) = (/) ) )
14 df-ne 
 |-  ( C =/= (/) <-> -. C = (/) )
15 xpeq0 
 |-  ( ( C X. B ) = (/) <-> ( C = (/) \/ B = (/) ) )
16 orel1 
 |-  ( -. C = (/) -> ( ( C = (/) \/ B = (/) ) -> B = (/) ) )
17 15 16 biimtrid 
 |-  ( -. C = (/) -> ( ( C X. B ) = (/) -> B = (/) ) )
18 14 17 sylbi 
 |-  ( C =/= (/) -> ( ( C X. B ) = (/) -> B = (/) ) )
19 18 adantr 
 |-  ( ( C =/= (/) /\ A = (/) ) -> ( ( C X. B ) = (/) -> B = (/) ) )
20 13 19 sylbid 
 |-  ( ( C =/= (/) /\ A = (/) ) -> ( ( C X. A ) = ( C X. B ) -> B = (/) ) )
21 eqtr3 
 |-  ( ( A = (/) /\ B = (/) ) -> A = B )
22 6 20 21 syl6an 
 |-  ( ( C =/= (/) /\ A = (/) ) -> ( ( C X. A ) = ( C X. B ) -> A = B ) )
23 5 22 sylan2b 
 |-  ( ( C =/= (/) /\ -. A =/= (/) ) -> ( ( C X. A ) = ( C X. B ) -> A = B ) )
24 xpeq2 
 |-  ( A = B -> ( C X. A ) = ( C X. B ) )
25 23 24 impbid1 
 |-  ( ( C =/= (/) /\ -. A =/= (/) ) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )
26 4 25 pm2.61dan 
 |-  ( C =/= (/) -> ( ( C X. A ) = ( C X. B ) <-> A = B ) )