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 ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 sdomdom ( 𝐵𝐴𝐵𝐴 )
2 infxpabs ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ 𝐴 )
3 infunabs ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴𝐵𝐴 ) → ( 𝐴𝐵 ) ≈ 𝐴 )
4 3 3expa ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵𝐴 ) → ( 𝐴𝐵 ) ≈ 𝐴 )
5 4 adantrl ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵𝐴 ) ) → ( 𝐴𝐵 ) ≈ 𝐴 )
6 5 ensymd ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵𝐴 ) ) → 𝐴 ≈ ( 𝐴𝐵 ) )
7 entr ( ( ( 𝐴 × 𝐵 ) ≈ 𝐴𝐴 ≈ ( 𝐴𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )
8 2 6 7 syl2anc ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ≠ ∅ ∧ 𝐵𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )
9 8 expr ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝐵 ≠ ∅ ) → ( 𝐵𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) ) )
10 9 adantrl ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) ) )
11 1 10 syl5 ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐵𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) ) )
12 domtri2 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )
13 12 ad2ant2r ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )
14 xpcomeng ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
15 14 ad2ant2r ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
16 simplrl ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → 𝐵 ∈ dom card )
17 domtr ( ( ω ≼ 𝐴𝐴𝐵 ) → ω ≼ 𝐵 )
18 17 ad4ant24 ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ω ≼ 𝐵 )
19 infn0 ( ω ≼ 𝐴𝐴 ≠ ∅ )
20 19 ad3antlr ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → 𝐴 ≠ ∅ )
21 simpr ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → 𝐴𝐵 )
22 infxpabs ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 𝐴 ≠ ∅ ∧ 𝐴𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 )
23 16 18 20 21 22 syl22anc ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ( 𝐵 × 𝐴 ) ≈ 𝐵 )
24 uncom ( 𝐴𝐵 ) = ( 𝐵𝐴 )
25 infunabs ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵𝐴𝐵 ) → ( 𝐵𝐴 ) ≈ 𝐵 )
26 16 18 21 25 syl3anc ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ( 𝐵𝐴 ) ≈ 𝐵 )
27 24 26 eqbrtrid ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ( 𝐴𝐵 ) ≈ 𝐵 )
28 27 ensymd ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → 𝐵 ≈ ( 𝐴𝐵 ) )
29 entr ( ( ( 𝐵 × 𝐴 ) ≈ 𝐵𝐵 ≈ ( 𝐴𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴𝐵 ) )
30 23 28 29 syl2anc ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴𝐵 ) )
31 entr ( ( ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )
32 15 30 31 syl2an2r ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) ∧ 𝐴𝐵 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )
33 32 ex ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴𝐵 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) ) )
34 13 33 sylbird ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( ¬ 𝐵𝐴 → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) ) )
35 11 34 pm2.61d ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝐵 ∈ dom card ∧ 𝐵 ≠ ∅ ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴𝐵 ) )