Metamath Proof Explorer

Theorem chscllem3

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ℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
chscllem3.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
chscllem3.8 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
chscllem3.9 ⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
chscllem3.10 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( 𝐶 +ℎ 𝐷 ) )
Assertion chscllem3 ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝑁 ) )

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 chscllem3.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 chscllem3.8 ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
9 chscllem3.9 ⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
10 chscllem3.10 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( 𝐶 +ℎ 𝐷 ) )
11 2fveq3 ⊢ ( 𝑛 = 𝑁 → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )
12 fvex ⊢ ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) ∈ V
13 11 6 12 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )
14 7 13 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) = ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) )
15 14 eqcomd ⊢ ( 𝜑 → ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( 𝐹 ‘ 𝑁 ) )
16 chsh ⊢ ( 𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
17 2 16 syl ⊢ ( 𝜑 → 𝐵 ∈ Sℋ )
18 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
19 1 18 syl ⊢ ( 𝜑 → 𝐴 ∈ Sℋ )
20 shocsh ⊢ ( 𝐴 ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
21 19 20 syl ⊢ ( 𝜑 → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
22 shless ⊢ ( ( ( 𝐵 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) ∧ 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
23 17 21 19 3 22 syl31anc ⊢ ( 𝜑 → ( 𝐵 +ℋ 𝐴 ) ⊆ ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
24 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
25 19 17 24 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
26 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ ( ⊥ ‘ 𝐴 ) ∈ Sℋ ) → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
27 19 21 26 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) +ℋ 𝐴 ) )
28 23 25 27 3sstr4d ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
29 4 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
30 28 29 sseldd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) )
31 pjpreeq ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐻 ‘ 𝑁 ) ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐴 ) ) ) → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( 𝐹 ‘ 𝑁 ) ↔ ( ( 𝐹 ‘ 𝑁 ) ∈ 𝐴 ∧ ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) )
32 1 30 31 syl2anc ⊢ ( 𝜑 → ( ( ( projℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑁 ) ) = ( 𝐹 ‘ 𝑁 ) ↔ ( ( 𝐹 ‘ 𝑁 ) ∈ 𝐴 ∧ ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) )
33 15 32 mpbid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑁 ) ∈ 𝐴 ∧ ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) )
34 33 simprd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) )
35 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐴 ∈ Sℋ )
36 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )
37 ocin ⊢ ( 𝐴 ∈ Sℋ → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )
38 19 37 syl ⊢ ( 𝜑 → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐴 ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )
40 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐶 ∈ 𝐴 )
41 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
42 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐷 ∈ 𝐵 )
43 41 42 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐷 ∈ ( ⊥ ‘ 𝐴 ) )
44 1 2 3 4 5 6 chscllem1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝐴 )
45 44 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ 𝐴 )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐹 ‘ 𝑁 ) ∈ 𝐴 )
47 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝑧 ∈ ( ⊥ ‘ 𝐴 ) )
48 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐻 ‘ 𝑁 ) = ( 𝐶 +ℎ 𝐷 ) )
49 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) )
50 48 49 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐶 +ℎ 𝐷 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) )
51 35 36 39 40 43 46 47 50 shuni ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → ( 𝐶 = ( 𝐹 ‘ 𝑁 ) ∧ 𝐷 = 𝑧 ) )
52 51 simpld ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ⊥ ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑁 ) +ℎ 𝑧 ) ) ) → 𝐶 = ( 𝐹 ‘ 𝑁 ) )
53 34 52 rexlimddv ⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝑁 ) )