Metamath Proof Explorer

Theorem cdj3lem3

Description: Lemma for cdj3i . Value of the second-component function T . (Contributed by NM, 23-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 ⊢ 𝐴 ∈ Sℋ
cdj3lem2.2 ⊢ 𝐵 ∈ Sℋ
cdj3lem3.3 ⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
Assertion cdj3lem3 ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢ 𝐴 ∈ Sℋ
2 cdj3lem2.2 ⊢ 𝐵 ∈ Sℋ
3 cdj3lem3.3 ⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
5 4 eqeq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ ( 𝐵 ∩ 𝐴 ) = 0ℋ )
6 2 sheli ⊢ ( 𝐷 ∈ 𝐵 → 𝐷 ∈ ℋ )
7 1 sheli ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ ℋ )
8 ax-hvcom ⊢ ( ( 𝐷 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐷 +ℎ 𝐶 ) = ( 𝐶 +ℎ 𝐷 ) )
9 6 7 8 syl2an ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐷 +ℎ 𝐶 ) = ( 𝐶 +ℎ 𝐷 ) )
10 9 fveq2d ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑇 ‘ ( 𝐷 +ℎ 𝐶 ) ) = ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) )
11 10 3adant3 ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐷 +ℎ 𝐶 ) ) = ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) )
12 2 1 shscomi ⊢ ( 𝐵 +ℋ 𝐴 ) = ( 𝐴 +ℋ 𝐵 )
13 2 sheli ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ )
14 1 sheli ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ )
15 ax-hvcom ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑤 ) )
16 13 14 15 syl2an ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑤 ) )
17 16 eqeq2d ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 = ( 𝑤 +ℎ 𝑧 ) ↔ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
18 17 rexbidva ⊢ ( 𝑤 ∈ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
19 18 riotabiia ⊢ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) = ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) )
20 12 19 mpteq12i ⊢ ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) ) = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
21 3 20 eqtr4i ⊢ 𝑇 = ( 𝑥 ∈ ( 𝐵 +ℋ 𝐴 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑤 +ℎ 𝑧 ) ) )
22 2 1 21 cdj3lem2 ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐷 +ℎ 𝐶 ) ) = 𝐷 )
23 11 22 eqtr3d ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) = 𝐷 )
24 5 23 syl3an3b ⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) = 𝐷 )
25 24 3com12 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝐶 +ℎ 𝐷 ) ) = 𝐷 )