Metamath Proof Explorer

Theorem infxp

Description: Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infxp 
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A X. B ) ~~ ( A u. B ) )

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( B ~< A -> B ~<_ A )
2 infxpabs 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ A )
3 infunabs 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~~ A )
4 3 3expa 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ B ~<_ A ) -> ( A u. B ) ~~ A )
5 4 adantrl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A u. B ) ~~ A )
6 5 ensymd 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> A ~~ ( A u. B ) )
7 entr 
 |-  ( ( ( A X. B ) ~~ A /\ A ~~ ( A u. B ) ) -> ( A X. B ) ~~ ( A u. B ) )
8 2 6 7 syl2anc 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ ( A u. B ) )
9 8 expr 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ B =/= (/) ) -> ( B ~<_ A -> ( A X. B ) ~~ ( A u. B ) ) )
10 9 adantrl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( B ~<_ A -> ( A X. B ) ~~ ( A u. B ) ) )
11 1 10 syl5 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( B ~< A -> ( A X. B ) ~~ ( A u. B ) ) )
12 domtri2 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) )
13 12 ad2ant2r 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A ~<_ B <-> -. B ~< A ) )
14 xpcomeng 
 |-  ( ( A e. dom card /\ B e. dom card ) -> ( A X. B ) ~~ ( B X. A ) )
15 14 ad2ant2r 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A X. B ) ~~ ( B X. A ) )
16 simplrl 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> B e. dom card )
17 domtr 
 |-  ( ( _om ~<_ A /\ A ~<_ B ) -> _om ~<_ B )
18 17 ad4ant24 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> _om ~<_ B )
19 infn0 
 |-  ( _om ~<_ A -> A =/= (/) )
20 19 ad3antlr 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> A =/= (/) )
21 simpr 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> A ~<_ B )
22 infxpabs 
 |-  ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( A =/= (/) /\ A ~<_ B ) ) -> ( B X. A ) ~~ B )
23 16 18 20 21 22 syl22anc 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B X. A ) ~~ B )
24 uncom 
 |-  ( A u. B ) = ( B u. A )
25 infunabs 
 |-  ( ( B e. dom card /\ _om ~<_ B /\ A ~<_ B ) -> ( B u. A ) ~~ B )
26 16 18 21 25 syl3anc 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B u. A ) ~~ B )
27 24 26 eqbrtrid 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( A u. B ) ~~ B )
28 27 ensymd 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> B ~~ ( A u. B ) )
29 entr 
 |-  ( ( ( B X. A ) ~~ B /\ B ~~ ( A u. B ) ) -> ( B X. A ) ~~ ( A u. B ) )
30 23 28 29 syl2anc 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B X. A ) ~~ ( A u. B ) )
31 entr 
 |-  ( ( ( A X. B ) ~~ ( B X. A ) /\ ( B X. A ) ~~ ( A u. B ) ) -> ( A X. B ) ~~ ( A u. B ) )
32 15 30 31 syl2an2r 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( A X. B ) ~~ ( A u. B ) )
33 32 ex 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A ~<_ B -> ( A X. B ) ~~ ( A u. B ) ) )
34 13 33 sylbird 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( -. B ~< A -> ( A X. B ) ~~ ( A u. B ) ) )
35 11 34 pm2.61d 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A X. B ) ~~ ( A u. B ) )