Metamath Proof Explorer

Theorem chscllem1

Description: Lemma for chscl . (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
chscl.4 ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
chscl.5 ⊢ ( 𝜑 → 𝐻 ⇝𝑣 𝑢 )
chscl.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
Assertion chscllem1 ( 𝜑 → 𝐹 : ℕ ⟶ 𝐴 )

Proof

Step Hyp Ref Expression
1 chscl.1 ⊢ ( 𝜑 → 𝐴 ∈ Cℋ )
2 chscl.2 ⊢ ( 𝜑 → 𝐵 ∈ Cℋ )
3 chscl.3 ⊢ ( 𝜑 → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
4 chscl.4 ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
5 chscl.5 ⊢ ( 𝜑 → 𝐻 ⇝𝑣 𝑢 )
6 chscl.6 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
7 eqid ⊢ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ Cℋ )
9 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
10 chsh ⊢ ( 𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
11 2 10 syl ⊢ ( 𝜑 → 𝐵 ∈ Sℋ )
12 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
13 1 12 syl ⊢ ( 𝜑 → 𝐴 ∈ Sℋ )
14 shocsh ⊢ ( 𝐴 ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
15 13 14 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
16 shless ⊢ ( ( ( 𝐵 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) ∧ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
17 11 15 13 3 16 syl31anc ⊢ ( 𝜑 → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
18 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
19 13 11 18 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
20 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ) → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
21 13 15 20 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
22 17 19 21 3sstr4d ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
23 22 sselda ⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ 𝑛 ) ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( 𝐻 ‘ 𝑛 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
24 9 23 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐻 ‘ 𝑛 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
25 pjpreeq ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐻 ‘ 𝑛 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ↔ ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑛 ) = ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) +ℎ 𝑥 ) ) ) )
26 8 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ↔ ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑛 ) = ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) +ℎ 𝑥 ) ) ) )
27 7 26 mpbii ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ∈ 𝐴 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑛 ) = ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) +ℎ 𝑥 ) ) )
28 27 simpld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) ∈ 𝐴 )
29 28 6 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝐴 )