Metamath Proof Explorer

Theorem pjjsi

Description: A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjjs.1 ⊢G∈Cℋ
pjjs.2 ⊢H∈Sℋ
Assertion pjjsi ⊢∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→G∨ℋH=G+ℋH

Proof

Step Hyp Ref Expression
1 pjjs.1 ⊢G∈Cℋ
2 pjjs.2 ⊢H∈Sℋ
3 fveq2 ⊢x=w→projℎ⁡⊥⁡G⁡x=projℎ⁡⊥⁡G⁡w
4 3 eleq1d ⊢x=w→projℎ⁡⊥⁡G⁡x∈H↔projℎ⁡⊥⁡G⁡w∈H
5 4 rspcv ⊢w∈G∨ℋH→∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→projℎ⁡⊥⁡G⁡w∈H
6 1 chshii ⊢G∈Sℋ
7 6 2 shjcli ⊢G∨ℋH∈Cℋ
8 7 cheli ⊢w∈G∨ℋH→w∈ℋ
9 1 pjcli ⊢w∈ℋ→projℎ⁡G⁡w∈G
10 9 anim1i ⊢w∈ℋ∧projℎ⁡⊥⁡G⁡w∈H→projℎ⁡G⁡w∈G∧projℎ⁡⊥⁡G⁡w∈H
11 axpjpj ⊢G∈Cℋ∧w∈ℋ→w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w
12 1 11 mpan ⊢w∈ℋ→w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w
13 12 adantr ⊢w∈ℋ∧projℎ⁡⊥⁡G⁡w∈H→w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w
14 10 13 jca ⊢w∈ℋ∧projℎ⁡⊥⁡G⁡w∈H→projℎ⁡G⁡w∈G∧projℎ⁡⊥⁡G⁡w∈H∧w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w
15 8 14 sylan ⊢w∈G∨ℋH∧projℎ⁡⊥⁡G⁡w∈H→projℎ⁡G⁡w∈G∧projℎ⁡⊥⁡G⁡w∈H∧w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w
16 rspceov ⊢projℎ⁡G⁡w∈G∧projℎ⁡⊥⁡G⁡w∈H∧w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w→∃y∈G∃z∈Hw=y+ℎz
17 16 3expa ⊢projℎ⁡G⁡w∈G∧projℎ⁡⊥⁡G⁡w∈H∧w=projℎ⁡G⁡w+ℎprojℎ⁡⊥⁡G⁡w→∃y∈G∃z∈Hw=y+ℎz
18 15 17 syl ⊢w∈G∨ℋH∧projℎ⁡⊥⁡G⁡w∈H→∃y∈G∃z∈Hw=y+ℎz
19 6 2 shseli ⊢w∈G+ℋH↔∃y∈G∃z∈Hw=y+ℎz
20 18 19 sylibr ⊢w∈G∨ℋH∧projℎ⁡⊥⁡G⁡w∈H→w∈G+ℋH
21 20 ex ⊢w∈G∨ℋH→projℎ⁡⊥⁡G⁡w∈H→w∈G+ℋH
22 5 21 syldc ⊢∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→w∈G∨ℋH→w∈G+ℋH
23 22 ssrdv ⊢∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→G∨ℋH⊆G+ℋH
24 6 2 shsleji ⊢G+ℋH⊆G∨ℋH
25 23 24 jctir ⊢∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→G∨ℋH⊆G+ℋH∧G+ℋH⊆G∨ℋH
26 eqss ⊢G∨ℋH=G+ℋH↔G∨ℋH⊆G+ℋH∧G+ℋH⊆G∨ℋH
27 25 26 sylibr ⊢∀x∈G∨ℋHprojℎ⁡⊥⁡G⁡x∈H→G∨ℋH=G+ℋH