Step |
Hyp |
Ref |
Expression |
1 |
|
3oalem1.1 |
⊢ 𝐵 ∈ Cℋ |
2 |
|
3oalem1.2 |
⊢ 𝐶 ∈ Cℋ |
3 |
|
3oalem1.3 |
⊢ 𝑅 ∈ Cℋ |
4 |
|
3oalem1.4 |
⊢ 𝑆 ∈ Cℋ |
5 |
1
|
cheli |
⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ ) |
6 |
3
|
cheli |
⊢ ( 𝑦 ∈ 𝑅 → 𝑦 ∈ ℋ ) |
7 |
5 6
|
anim12i |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) |
8 |
|
hvaddcl |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ) |
9 |
|
eleq1 |
⊢ ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑣 ∈ ℋ ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ) ) |
10 |
8 9
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → 𝑣 ∈ ℋ ) ) |
11 |
10
|
imdistani |
⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ) |
12 |
7 11
|
sylan |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ) |
13 |
2
|
cheli |
⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ ) |
14 |
4
|
cheli |
⊢ ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ℋ ) |
15 |
13 14
|
anim12i |
⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) |
17 |
12 16
|
anim12i |
⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ) |