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

Metamath Proof Explorer

Theorem shscli

Description: Closure of subspace sum. (Contributed by NM, 15-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses shscl.1 ⊢ 𝐴 ∈ Sℋ
shscl.2 ⊢ 𝐵 ∈ Sℋ
Assertion shscli ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ

Proof

Step Hyp Ref Expression
1 shscl.1 ⊢ 𝐴 ∈ Sℋ
2 shscl.2 ⊢ 𝐵 ∈ Sℋ
3 shsss ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )
4 1 2 3 mp2an ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ
5 sh0 ⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 )
6 1 5 ax-mp ⊢ 0ℎ ∈ 𝐴
7 sh0 ⊢ ( 𝐵 ∈ Sℋ → 0ℎ ∈ 𝐵 )
8 2 7 ax-mp ⊢ 0ℎ ∈ 𝐵
9 ax-hv0cl ⊢ 0ℎ ∈ ℋ
10 9 hvaddlidi ⊢ ( 0ℎ +ℎ 0ℎ ) = 0ℎ
11 10 eqcomi ⊢ 0ℎ = ( 0ℎ +ℎ 0ℎ )
12 rspceov ⊢ ( ( 0ℎ ∈ 𝐴 ∧ 0ℎ ∈ 𝐵 ∧ 0ℎ = ( 0ℎ +ℎ 0ℎ ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 0ℎ = ( 𝑥 +ℎ 𝑦 ) )
13 6 8 11 12 mp3an ⊢ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 0ℎ = ( 𝑥 +ℎ 𝑦 )
14 1 2 shseli ⊢ ( 0ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 0ℎ = ( 𝑥 +ℎ 𝑦 ) )
15 13 14 mpbir ⊢ 0ℎ ∈ ( 𝐴 +ℋ 𝐵 )
16 4 15 pm3.2i ⊢ ( ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ ∧ 0ℎ ∈ ( 𝐴 +ℋ 𝐵 ) )
17 1 2 shseli ⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) )
18 1 2 shseli ⊢ ( 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) )
19 shaddcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑧 +ℎ 𝑣 ) ∈ 𝐴 )
20 1 19 mp3an1 ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑧 +ℎ 𝑣 ) ∈ 𝐴 )
21 20 ad2ant2r ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑧 +ℎ 𝑣 ) ∈ 𝐴 )
22 21 ad2ant2r ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑧 +ℎ 𝑣 ) ∈ 𝐴 )
23 shaddcl ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑤 +ℎ 𝑢 ) ∈ 𝐵 )
24 2 23 mp3an1 ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑤 +ℎ 𝑢 ) ∈ 𝐵 )
25 24 ad2ant2l ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑤 +ℎ 𝑢 ) ∈ 𝐵 )
26 25 ad2ant2r ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑤 +ℎ 𝑢 ) ∈ 𝐵 )
27 oveq12 ⊢ ( ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
28 27 ad2ant2l ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 +ℎ 𝑦 ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
29 1 sheli ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ )
30 1 sheli ⊢ ( 𝑣 ∈ 𝐴 → 𝑣 ∈ ℋ )
31 29 30 anim12i ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑧 ∈ ℋ ∧ 𝑣 ∈ ℋ ) )
32 2 sheli ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ )
33 2 sheli ⊢ ( 𝑢 ∈ 𝐵 → 𝑢 ∈ ℋ )
34 32 33 anim12i ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ ) )
35 hvadd4 ⊢ ( ( ( 𝑧 ∈ ℋ ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
36 31 34 35 syl2an ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
37 36 an4s ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
38 37 ad2ant2r ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) = ( ( 𝑧 +ℎ 𝑤 ) +ℎ ( 𝑣 +ℎ 𝑢 ) ) )
39 28 38 eqtr4d ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 +ℎ 𝑦 ) = ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) )
40 rspceov ⊢ ( ( ( 𝑧 +ℎ 𝑣 ) ∈ 𝐴 ∧ ( 𝑤 +ℎ 𝑢 ) ∈ 𝐵 ∧ ( 𝑥 +ℎ 𝑦 ) = ( ( 𝑧 +ℎ 𝑣 ) +ℎ ( 𝑤 +ℎ 𝑢 ) ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
41 22 26 39 40 syl3anc ⊢ ( ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
42 41 ancoms ⊢ ( ( ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
43 42 exp43 ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ) ) )
44 43 rexlimivv ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ) )
45 44 com3l ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ) )
46 45 rexlimivv ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) )
47 46 imp ⊢ ( ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ∧ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
48 17 18 47 syl2anb ⊢ ( ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
49 1 2 shseli ⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
50 48 49 sylibr ⊢ ( ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
51 50 rgen2 ⊢ ∀ 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 )
52 shmulcl ⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴 ) → ( 𝑥 ·ℎ 𝑣 ) ∈ 𝐴 )
53 1 52 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴 ) → ( 𝑥 ·ℎ 𝑣 ) ∈ 𝐴 )
54 53 adantrr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 ·ℎ 𝑣 ) ∈ 𝐴 )
55 shmulcl ⊢ ( ( 𝐵 ∈ Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑢 ∈ 𝐵 ) → ( 𝑥 ·ℎ 𝑢 ) ∈ 𝐵 )
56 2 55 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑢 ∈ 𝐵 ) → ( 𝑥 ·ℎ 𝑢 ) ∈ 𝐵 )
57 56 adantrr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 ·ℎ 𝑢 ) ∈ 𝐵 )
58 57 adantrl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 ·ℎ 𝑢 ) ∈ 𝐵 )
59 oveq2 ⊢ ( 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) )
60 59 adantl ⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) )
61 60 ad2antll ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 ·ℎ 𝑦 ) = ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) )
62 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
63 ax-hvdistr1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) )
64 62 30 33 63 syl3an ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) )
65 64 3expb ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) )
66 65 adantrrr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 ·ℎ ( 𝑣 +ℎ 𝑢 ) ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) )
67 61 66 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 ·ℎ 𝑦 ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) )
68 rspceov ⊢ ( ( ( 𝑥 ·ℎ 𝑣 ) ∈ 𝐴 ∧ ( 𝑥 ·ℎ 𝑢 ) ∈ 𝐵 ∧ ( 𝑥 ·ℎ 𝑦 ) = ( ( 𝑥 ·ℎ 𝑣 ) +ℎ ( 𝑥 ·ℎ 𝑢 ) ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
69 54 58 67 68 syl3anc ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
70 69 ancoms ⊢ ( ( ( 𝑣 ∈ 𝐴 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) ) ∧ 𝑥 ∈ ℂ ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
71 70 exp42 ⊢ ( 𝑣 ∈ 𝐴 → ( 𝑢 ∈ 𝐵 → ( 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑥 ∈ ℂ → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ) ) )
72 71 imp ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) → ( 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑥 ∈ ℂ → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ) )
73 72 rexlimivv ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) → ( 𝑥 ∈ ℂ → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) )
74 73 impcom ⊢ ( ( 𝑥 ∈ ℂ ∧ ∃ 𝑣 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑦 = ( 𝑣 +ℎ 𝑢 ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
75 18 74 sylan2b ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
76 1 2 shseli ⊢ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑥 ·ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) )
77 75 76 sylibr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
78 77 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 )
79 51 78 pm3.2i ⊢ ( ∀ 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) )
80 issh2 ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ↔ ( ( ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ ∧ 0ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ) ∧ ( ∀ 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( 𝐴 +ℋ 𝐵 ) ) ) )
81 16 79 80 mpbir2an ⊢ ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ