Theorem cdj3lem2a

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

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

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	⊢ 𝐴 ∈ Sℋ
2		cdj3lem2.2	⊢ 𝐵 ∈ Sℋ
3		cdj3lem2.3	⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4	1 2	shseli	⊢ ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝐶 = ( 𝑣 +ℎ 𝑢 ) )
5	1 2 3	cdj3lem2	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑣 +ℎ 𝑢 ) ) = 𝑣 )
6		simp1	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝑣 ∈ 𝐴 )
7	5 6	eqeltrd	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐴 )
8	7	3expa	⊢ ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐴 )
9		fveq2	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ ( 𝑣 +ℎ 𝑢 ) ) )
10	9	eleq1d	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ↔ ( 𝑆 ‘ ( 𝑣 +ℎ 𝑢 ) ) ∈ 𝐴 ) )
11	8 10	syl5ibr	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ) )
12	11	expd	⊢ ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ) ) )
13	12	com13	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ) ) )
14	13	rexlimdvv	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝐶 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ) )
15	4 14	syl5bi	⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 ) )
16	15	impcom	⊢ ( ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ 𝐶 ) ∈ 𝐴 )