Theorem shsel3

Description: Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	shsel3	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		shsel	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) ) )
2		id	⊢ ( 𝐶 = ( 𝑥 +ℎ 𝑧 ) → 𝐶 = ( 𝑥 +ℎ 𝑧 ) )
3		shel	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℋ )
4		shel	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℋ )
5		hvaddsubval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 +ℎ 𝑧 ) = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
6	3 4 5	syl2an	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 +ℎ 𝑧 ) = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
7	6	an4s	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑥 +ℎ 𝑧 ) = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
8	7	anassrs	⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 +ℎ 𝑧 ) = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
9	2 8	sylan9eqr	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 +ℎ 𝑧 ) ) → 𝐶 = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
10		neg1cn	⊢ - 1 ∈ ℂ
11		shmulcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝑧 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
12	10 11	mp3an2	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑧 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
13	12	adantll	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑧 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
14	13	adantlr	⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 )
15		oveq2	⊢ ( 𝑦 = ( - 1 ·ℎ 𝑧 ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) )
16	15	rspceeqv	⊢ ( ( ( - 1 ·ℎ 𝑧 ) ∈ 𝐵 ∧ 𝐶 = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) )
17	14 16	sylan	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 −ℎ ( - 1 ·ℎ 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) )
18	9 17	syldan	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 +ℎ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) )
19	18	rexlimdva2	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) → ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )
20		id	⊢ ( 𝐶 = ( 𝑥 −ℎ 𝑦 ) → 𝐶 = ( 𝑥 −ℎ 𝑦 ) )
21		shel	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℋ )
22		hvsubval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
23	3 21 22	syl2an	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐵 ∈ Sℋ ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
24	23	an4s	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
25	24	anassrs	⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 −ℎ 𝑦 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
26	20 25	sylan9eqr	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) → 𝐶 = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
27		shmulcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝑦 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑦 ) ∈ 𝐵 )
28	10 27	mp3an2	⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑦 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑦 ) ∈ 𝐵 )
29	28	adantll	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑦 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑦 ) ∈ 𝐵 )
30	29	adantlr	⊢ ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( - 1 ·ℎ 𝑦 ) ∈ 𝐵 )
31		oveq2	⊢ ( 𝑧 = ( - 1 ·ℎ 𝑦 ) → ( 𝑥 +ℎ 𝑧 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
32	31	rspceeqv	⊢ ( ( ( - 1 ·ℎ 𝑦 ) ∈ 𝐵 ∧ 𝐶 = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) )
33	30 32	sylan	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) )
34	26 33	syldan	⊢ ( ( ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) )
35	34	rexlimdva2	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) → ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) ) )
36	19 35	impbid	⊢ ( ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )
37	36	rexbidva	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )
38	1 37	bitrd	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )