Metamath Proof Explorer

Theorem cdj3lem2

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

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

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢ 𝐴 ∈ Sℋ
2 cdj3lem2.2 ⊢ 𝐵 ∈ Sℋ
3 cdj3lem2.3 ⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4 1 2 shsvai ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
5 eqeq1 ⊢ ( 𝑥 = ( 𝐶 +ℎ 𝐷 ) → ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
6 5 rexbidv ⊢ ( 𝑥 = ( 𝐶 +ℎ 𝐷 ) → ( ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
7 6 riotabidv ⊢ ( 𝑥 = ( 𝐶 +ℎ 𝐷 ) → ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) = ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
8 riotaex ⊢ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) ∈ V
9 7 3 8 fvmpt ⊢ ( ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝑆 ‘ ( 𝐶 +ℎ 𝐷 ) ) = ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
10 4 9 syl ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝐶 +ℎ 𝐷 ) ) = ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
11 10 3adant3 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝐶 +ℎ 𝐷 ) ) = ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) )
12 eqid ⊢ ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝐷 )
13 oveq2 ⊢ ( 𝑤 = 𝐷 → ( 𝐶 +ℎ 𝑤 ) = ( 𝐶 +ℎ 𝐷 ) )
14 13 rspceeqv ⊢ ( ( 𝐷 ∈ 𝐵 ∧ ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝐷 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) )
15 12 14 mpan2 ⊢ ( 𝐷 ∈ 𝐵 → ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) )
16 15 3ad2ant2 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) )
17 simp1 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝐶 ∈ 𝐴 )
18 1 2 cdjreui ⊢ ( ( ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃! 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) )
19 4 18 stoic3 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ∃! 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) )
20 oveq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 +ℎ 𝑤 ) = ( 𝐶 +ℎ 𝑤 ) )
21 20 eqeq2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) ) )
22 21 rexbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) ) )
23 22 riota2 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∃! 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) ↔ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) = 𝐶 ) )
24 17 19 23 syl2anc ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝑤 ) ↔ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) = 𝐶 ) )
25 16 24 mpbid ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑧 +ℎ 𝑤 ) ) = 𝐶 )
26 11 25 eqtrd ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝐶 +ℎ 𝐷 ) ) = 𝐶 )