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ℋ