This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 −ℎ 𝑦 ) ) )