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 ⊢ 𝐺 ∈ Cℋ
pjjs.2 ⊢ 𝐻 ∈ Sℋ
Assertion pjjsi ( ∀ 𝑥 ∈ ( 𝐺 ∨ℋ 𝐻 ) ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝑥 ) ∈ 𝐻 → ( 𝐺 ∨ℋ 𝐻 ) = ( 𝐺 +ℋ 𝐻 ) )

Proof

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