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 ⊢A∈Sℋ∧B∈Sℋ→C∈A+ℋB↔∃x∈A∃y∈BC=x-ℎy

Proof

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