This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chscllem4

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ℎ ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
chscl.7 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐵 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
Assertion chscllem4 ( 𝜑 → 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) )

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 chscl.7 ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( ( projℎ ‘ 𝐵 ) ‘ ( 𝐻 ‘ 𝑛 ) ) )
8 hlimf ⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ
9 ffun ⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ → Fun ⇝𝑣 )
10 8 9 ax-mp ⊢ Fun ⇝𝑣
11 funbrfv ⊢ ( Fun ⇝𝑣 → ( 𝐻 ⇝𝑣 𝑢 → ( ⇝𝑣 ‘ 𝐻 ) = 𝑢 ) )
12 10 5 11 mpsyl ⊢ ( 𝜑 → ( ⇝𝑣 ‘ 𝐻 ) = 𝑢 )
13 4 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑘 ∈ ℕ ↦ ( 𝐻 ‘ 𝑘 ) ) )
14 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
15 chsh ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ )
16 1 15 syl ⊢ ( 𝜑 → 𝐴 ∈ Sℋ )
17 chsh ⊢ ( 𝐵 ∈ Cℋ → 𝐵 ∈ Sℋ )
18 2 17 syl ⊢ ( 𝜑 → 𝐵 ∈ Sℋ )
19 shsel ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) )
20 16 18 19 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑘 ) ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) )
21 20 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐻 ‘ 𝑘 ) ∈ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) )
22 14 21 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) )
23 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) )
24 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝜑 )
25 24 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐴 ∈ Cℋ )
26 24 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐵 ∈ Cℋ )
27 24 3 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) )
28 24 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) )
29 24 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐻 ⇝𝑣 𝑢 )
30 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑘 ∈ ℕ )
31 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
32 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑦 ∈ 𝐵 )
33 25 26 27 28 29 6 30 31 32 23 chscllem3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑥 = ( 𝐹 ‘ 𝑘 ) )
34 chsscon2 ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) )
35 2 1 34 syl2anc ⊢ ( 𝜑 → ( 𝐵 ⊆ ( ⊥ ‘ 𝐴 ) ↔ 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) )
36 3 35 mpbid ⊢ ( 𝜑 → 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) )
37 24 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) )
38 shscom ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
39 16 18 38 syl2anc ⊢ ( 𝜑 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐵 +ℋ 𝐴 ) )
40 39 feq3d ⊢ ( 𝜑 → ( 𝐻 : ℕ ⟶ ( 𝐴 +ℋ 𝐵 ) ↔ 𝐻 : ℕ ⟶ ( 𝐵 +ℋ 𝐴 ) ) )
41 4 40 mpbid ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 𝐵 +ℋ 𝐴 ) )
42 24 41 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐻 : ℕ ⟶ ( 𝐵 +ℋ 𝐴 ) )
43 shss ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ )
44 16 43 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℋ )
45 24 44 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐴 ⊆ ℋ )
46 45 31 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑥 ∈ ℋ )
47 shss ⊢ ( 𝐵 ∈ Sℋ → 𝐵 ⊆ ℋ )
48 18 47 syl ⊢ ( 𝜑 → 𝐵 ⊆ ℋ )
49 24 48 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝐵 ⊆ ℋ )
50 49 32 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑦 ∈ ℋ )
51 ax-hvcom ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
52 46 50 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
53 23 52 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝑦 +ℎ 𝑥 ) )
54 26 25 37 42 29 7 30 32 31 53 chscllem3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → 𝑦 = ( 𝐺 ‘ 𝑘 ) )
55 33 54 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) )
56 23 55 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) )
57 56 3exp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) ) )
58 57 rexlimdvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐻 ‘ 𝑘 ) = ( 𝑥 +ℎ 𝑦 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) )
59 22 58 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) )
60 59 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( 𝐻 ‘ 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) )
61 13 60 eqtrd ⊢ ( 𝜑 → 𝐻 = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) )
62 1 2 3 4 5 6 chscllem1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝐴 )
63 62 44 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℋ )
64 2 1 36 41 5 7 chscllem1 ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝐵 )
65 64 48 fssd ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ℋ )
66 1 2 3 4 5 6 chscllem2 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝𝑣 )
67 funfvbrb ⊢ ( Fun ⇝𝑣 → ( 𝐹 ∈ dom ⇝𝑣 ↔ 𝐹 ⇝𝑣 ( ⇝𝑣 ‘ 𝐹 ) ) )
68 10 67 ax-mp ⊢ ( 𝐹 ∈ dom ⇝𝑣 ↔ 𝐹 ⇝𝑣 ( ⇝𝑣 ‘ 𝐹 ) )
69 66 68 sylib ⊢ ( 𝜑 → 𝐹 ⇝𝑣 ( ⇝𝑣 ‘ 𝐹 ) )
70 2 1 36 41 5 7 chscllem2 ⊢ ( 𝜑 → 𝐺 ∈ dom ⇝𝑣 )
71 funfvbrb ⊢ ( Fun ⇝𝑣 → ( 𝐺 ∈ dom ⇝𝑣 ↔ 𝐺 ⇝𝑣 ( ⇝𝑣 ‘ 𝐺 ) ) )
72 10 71 ax-mp ⊢ ( 𝐺 ∈ dom ⇝𝑣 ↔ 𝐺 ⇝𝑣 ( ⇝𝑣 ‘ 𝐺 ) )
73 70 72 sylib ⊢ ( 𝜑 → 𝐺 ⇝𝑣 ( ⇝𝑣 ‘ 𝐺 ) )
74 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) )
75 63 65 69 73 74 hlimadd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑘 ) +ℎ ( 𝐺 ‘ 𝑘 ) ) ) ⇝𝑣 ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) )
76 61 75 eqbrtrd ⊢ ( 𝜑 → 𝐻 ⇝𝑣 ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) )
77 funbrfv ⊢ ( Fun ⇝𝑣 → ( 𝐻 ⇝𝑣 ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) → ( ⇝𝑣 ‘ 𝐻 ) = ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) ) )
78 10 76 77 mpsyl ⊢ ( 𝜑 → ( ⇝𝑣 ‘ 𝐻 ) = ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) )
79 12 78 eqtr3d ⊢ ( 𝜑 → 𝑢 = ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) )
80 fvex ⊢ ( ⇝𝑣 ‘ 𝐹 ) ∈ V
81 80 chlimi ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐹 : ℕ ⟶ 𝐴 ∧ 𝐹 ⇝𝑣 ( ⇝𝑣 ‘ 𝐹 ) ) → ( ⇝𝑣 ‘ 𝐹 ) ∈ 𝐴 )
82 1 62 69 81 syl3anc ⊢ ( 𝜑 → ( ⇝𝑣 ‘ 𝐹 ) ∈ 𝐴 )
83 fvex ⊢ ( ⇝𝑣 ‘ 𝐺 ) ∈ V
84 83 chlimi ⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐺 : ℕ ⟶ 𝐵 ∧ 𝐺 ⇝𝑣 ( ⇝𝑣 ‘ 𝐺 ) ) → ( ⇝𝑣 ‘ 𝐺 ) ∈ 𝐵 )
85 2 64 73 84 syl3anc ⊢ ( 𝜑 → ( ⇝𝑣 ‘ 𝐺 ) ∈ 𝐵 )
86 shsva ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( ( ⇝𝑣 ‘ 𝐹 ) ∈ 𝐴 ∧ ( ⇝𝑣 ‘ 𝐺 ) ∈ 𝐵 ) → ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )
87 16 18 86 syl2anc ⊢ ( 𝜑 → ( ( ( ⇝𝑣 ‘ 𝐹 ) ∈ 𝐴 ∧ ( ⇝𝑣 ‘ 𝐺 ) ∈ 𝐵 ) → ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )
88 82 85 87 mp2and ⊢ ( 𝜑 → ( ( ⇝𝑣 ‘ 𝐹 ) +ℎ ( ⇝𝑣 ‘ 𝐺 ) ) ∈ ( 𝐴 +ℋ 𝐵 ) )
89 79 88 eqeltrd ⊢ ( 𝜑 → 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) )