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 ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 × ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 × 𝐵 ) ⊔ ( 𝐴 × 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 enrefg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ≈ 𝐴 )
3 0ex ⊢ ∅ ∈ V
4 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 )
5 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
6 3 4 5 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { ∅ } × 𝐵 ) ≈ 𝐵 )
7 6 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ≈ ( { ∅ } × 𝐵 ) )
8 xpen ⊢ ( ( 𝐴 ≈ 𝐴 ∧ 𝐵 ≈ ( { ∅ } × 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 × ( { ∅ } × 𝐵 ) ) )
9 2 7 8 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 × ( { ∅ } × 𝐵 ) ) )
10 1on ⊢ 1o ∈ On
11 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
12 xpsnen2g ⊢ ( ( 1o ∈ On ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
13 10 11 12 sylancr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( { 1o } × 𝐶 ) ≈ 𝐶 )
14 13 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ≈ ( { 1o } × 𝐶 ) )
15 xpen ⊢ ( ( 𝐴 ≈ 𝐴 ∧ 𝐶 ≈ ( { 1o } × 𝐶 ) ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐴 × ( { 1o } × 𝐶 ) ) )
16 2 14 15 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 × 𝐶 ) ≈ ( 𝐴 × ( { 1o } × 𝐶 ) ) )
17 xp01disjl ⊢ ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) = ∅
18 17 xpeq2i ⊢ ( 𝐴 × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( 𝐴 × ∅ )
19 xpindi ⊢ ( 𝐴 × ( ( { ∅ } × 𝐵 ) ∩ ( { 1o } × 𝐶 ) ) ) = ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∩ ( 𝐴 × ( { 1o } × 𝐶 ) ) )
20 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
21 18 19 20 3eqtr3i ⊢ ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∩ ( 𝐴 × ( { 1o } × 𝐶 ) ) ) = ∅
22 21 a1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∩ ( 𝐴 × ( { 1o } × 𝐶 ) ) ) = ∅ )
23 djuenun ⊢ ( ( ( 𝐴 × 𝐵 ) ≈ ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∧ ( 𝐴 × 𝐶 ) ≈ ( 𝐴 × ( { 1o } × 𝐶 ) ) ∧ ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∩ ( 𝐴 × ( { 1o } × 𝐶 ) ) ) = ∅ ) → ( ( 𝐴 × 𝐵 ) ⊔ ( 𝐴 × 𝐶 ) ) ≈ ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∪ ( 𝐴 × ( { 1o } × 𝐶 ) ) ) )
24 9 16 22 23 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 × 𝐵 ) ⊔ ( 𝐴 × 𝐶 ) ) ≈ ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∪ ( 𝐴 × ( { 1o } × 𝐶 ) ) ) )
25 df-dju ⊢ ( 𝐵 ⊔ 𝐶 ) = ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) )
26 25 xpeq2i ⊢ ( 𝐴 × ( 𝐵 ⊔ 𝐶 ) ) = ( 𝐴 × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) )
27 xpundi ⊢ ( 𝐴 × ( ( { ∅ } × 𝐵 ) ∪ ( { 1o } × 𝐶 ) ) ) = ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∪ ( 𝐴 × ( { 1o } × 𝐶 ) ) )
28 26 27 eqtri ⊢ ( 𝐴 × ( 𝐵 ⊔ 𝐶 ) ) = ( ( 𝐴 × ( { ∅ } × 𝐵 ) ) ∪ ( 𝐴 × ( { 1o } × 𝐶 ) ) )
29 24 28 breqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 × 𝐵 ) ⊔ ( 𝐴 × 𝐶 ) ) ≈ ( 𝐴 × ( 𝐵 ⊔ 𝐶 ) ) )
30 29 ensymd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 × ( 𝐵 ⊔ 𝐶 ) ) ≈ ( ( 𝐴 × 𝐵 ) ⊔ ( 𝐴 × 𝐶 ) ) )