Metamath Proof Explorer

Theorem xpdjuen

Description: Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of Enderton p. 142. (Contributed by NM, 26-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion xpdjuen 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. ( B |_| C ) ) ~~ ( ( A X. B ) |_| ( A X. C ) ) )

Proof

Step Hyp Ref Expression
1 enrefg 
 |-  ( A e. V -> A ~~ A )
2 1 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> A ~~ A )
3 0ex 
 |-  (/) e. _V
4 simp2 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> B e. W )
5 xpsnen2g 
 |-  ( ( (/) e. _V /\ B e. W ) -> ( { (/) } X. B ) ~~ B )
6 3 4 5 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { (/) } X. B ) ~~ B )
7 6 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> B ~~ ( { (/) } X. B ) )
8 xpen 
 |-  ( ( A ~~ A /\ B ~~ ( { (/) } X. B ) ) -> ( A X. B ) ~~ ( A X. ( { (/) } X. B ) ) )
9 2 7 8 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. B ) ~~ ( A X. ( { (/) } X. B ) ) )
10 1on 
 |-  1o e. On
11 simp3 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C e. X )
12 xpsnen2g 
 |-  ( ( 1o e. On /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
13 10 11 12 sylancr 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( { 1o } X. C ) ~~ C )
14 13 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> C ~~ ( { 1o } X. C ) )
15 xpen 
 |-  ( ( A ~~ A /\ C ~~ ( { 1o } X. C ) ) -> ( A X. C ) ~~ ( A X. ( { 1o } X. C ) ) )
16 2 14 15 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. C ) ~~ ( A X. ( { 1o } X. C ) ) )
17 xp01disjl 
 |-  ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) = (/)
18 17 xpeq2i 
 |-  ( A X. ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) ) = ( A X. (/) )
19 xpindi 
 |-  ( A X. ( ( { (/) } X. B ) i^i ( { 1o } X. C ) ) ) = ( ( A X. ( { (/) } X. B ) ) i^i ( A X. ( { 1o } X. C ) ) )
20 xp0 
 |-  ( A X. (/) ) = (/)
21 18 19 20 3eqtr3i 
 |-  ( ( A X. ( { (/) } X. B ) ) i^i ( A X. ( { 1o } X. C ) ) ) = (/)
22 21 a1i 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A X. ( { (/) } X. B ) ) i^i ( A X. ( { 1o } X. C ) ) ) = (/) )
23 djuenun 
 |-  ( ( ( A X. B ) ~~ ( A X. ( { (/) } X. B ) ) /\ ( A X. C ) ~~ ( A X. ( { 1o } X. C ) ) /\ ( ( A X. ( { (/) } X. B ) ) i^i ( A X. ( { 1o } X. C ) ) ) = (/) ) -> ( ( A X. B ) |_| ( A X. C ) ) ~~ ( ( A X. ( { (/) } X. B ) ) u. ( A X. ( { 1o } X. C ) ) ) )
24 9 16 22 23 syl3anc 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A X. B ) |_| ( A X. C ) ) ~~ ( ( A X. ( { (/) } X. B ) ) u. ( A X. ( { 1o } X. C ) ) ) )
25 df-dju 
 |-  ( B |_| C ) = ( ( { (/) } X. B ) u. ( { 1o } X. C ) )
26 25 xpeq2i 
 |-  ( A X. ( B |_| C ) ) = ( A X. ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) )
27 xpundi 
 |-  ( A X. ( ( { (/) } X. B ) u. ( { 1o } X. C ) ) ) = ( ( A X. ( { (/) } X. B ) ) u. ( A X. ( { 1o } X. C ) ) )
28 26 27 eqtri 
 |-  ( A X. ( B |_| C ) ) = ( ( A X. ( { (/) } X. B ) ) u. ( A X. ( { 1o } X. C ) ) )
29 24 28 breqtrrdi 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A X. B ) |_| ( A X. C ) ) ~~ ( A X. ( B |_| C ) ) )
30 29 ensymd 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. ( B |_| C ) ) ~~ ( ( A X. B ) |_| ( A X. C ) ) )