Metamath Proof Explorer


Theorem xpcan

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

Ref Expression
Assertion xpcan C C × A = C × B A = B

Proof

Step Hyp Ref Expression
1 xp11 C A C × A = C × 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 × A = C × B A = B
5 nne ¬ A A =
6 simpr C A = A =
7 xpeq2 A = C × A = C ×
8 xp0 C × =
9 7 8 eqtrdi A = C × A =
10 9 eqeq1d A = C × A = C × B = C × B
11 eqcom = C × B C × B =
12 10 11 bitrdi A = C × A = C × B C × B =
13 12 adantl C A = C × A = C × B C × B =
14 df-ne C ¬ C =
15 xpeq0 C × B = C = B =
16 orel1 ¬ C = C = B = B =
17 15 16 syl5bi ¬ C = C × B = B =
18 14 17 sylbi C C × B = B =
19 18 adantr C A = C × B = B =
20 13 19 sylbid C A = C × A = C × B B =
21 eqtr3 A = B = A = B
22 6 20 21 syl6an C A = C × A = C × B A = B
23 5 22 sylan2b C ¬ A C × A = C × B A = B
24 xpeq2 A = B C × A = C × B
25 23 24 impbid1 C ¬ A C × A = C × B A = B
26 4 25 pm2.61dan C C × A = C × B A = B