Metamath Proof Explorer

Theorem pjpjpre

Description: Decomposition of a vector into projections. This formulation of axpjpj avoids pjhth . (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses pjpjpre.1 ⊢ ( 𝜑 → 𝐻 ∈ Cℋ )
pjpjpre.2 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) )
Assertion pjpjpre ( 𝜑 → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pjpjpre.1 ⊢ ( 𝜑 → 𝐻 ∈ Cℋ )
2 pjpjpre.2 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) )
3 chsh ⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
4 1 3 syl ⊢ ( 𝜑 → 𝐻 ∈ Sℋ )
5 shocsh ⊢ ( 𝐻 ∈ Sℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
6 4 5 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
7 shsel ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ) → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
8 4 6 7 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
9 2 8 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
10 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
11 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝑥 ∈ 𝐻 )
12 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝑦 ∈ ( ⊥ ‘ 𝐻 ) )
13 rspe ⊢ ( ( 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) → ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
14 12 10 13 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) )
15 pjpreeq ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝑥 ↔ ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) )
16 1 2 15 syl2anc ⊢ ( 𝜑 → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝑥 ↔ ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝑥 ↔ ( 𝑥 ∈ 𝐻 ∧ ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) )
18 11 14 17 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝑥 )
19 shococss ⊢ ( 𝐻 ∈ Sℋ → 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
20 4 19 syl ⊢ ( 𝜑 → 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
22 21 11 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐻 ∈ Cℋ )
24 23 3 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐻 ∈ Sℋ )
25 shel ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ ℋ )
26 24 11 25 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝑥 ∈ ℋ )
27 24 5 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
28 shel ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝑦 ∈ ℋ )
29 27 12 28 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝑦 ∈ ℋ )
30 ax-hvcom ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
31 26 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
32 10 31 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
33 rspe ⊢ ( ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
34 22 32 33 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
35 choccl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
36 1 35 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
37 shocsh ⊢ ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ∈ Sℋ )
38 6 37 syl ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ∈ Sℋ )
39 shless ⊢ ( ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ) ∧ 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) +ℋ ( ⊥ ‘ 𝐻 ) ) )
40 4 38 6 20 39 syl31anc ⊢ ( 𝜑 → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) +ℋ ( ⊥ ‘ 𝐻 ) ) )
41 shscom ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ∈ Sℋ ) → ( ( ⊥ ‘ 𝐻 ) +ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) +ℋ ( ⊥ ‘ 𝐻 ) ) )
42 6 38 41 syl2anc ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝐻 ) +ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) +ℋ ( ⊥ ‘ 𝐻 ) ) )
43 40 42 sseqtrrd ⊢ ( 𝜑 → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ⊆ ( ( ⊥ ‘ 𝐻 ) +ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) )
44 43 2 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( ( ⊥ ‘ 𝐻 ) +ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) )
45 pjpreeq ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝐴 ∈ ( ( ⊥ ‘ 𝐻 ) +ℋ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝑦 ↔ ( 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∧ ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ) )
46 36 44 45 syl2anc ⊢ ( 𝜑 → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝑦 ↔ ( 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∧ ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝑦 ↔ ( 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∧ ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ) )
48 12 34 47 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 𝑦 )
49 18 48 oveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = ( 𝑥 +ℎ 𝑦 ) )
50 10 49 eqtr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
51 50 exp32 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 = ( 𝑥 +ℎ 𝑦 ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ) )
52 51 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐻 ∃ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑥 +ℎ 𝑦 ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) )
53 9 52 mpd ⊢ ( 𝜑 → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )