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 ) )