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 hvaddid2i ( 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