Proof of Theorem 3oalem2
| Step | Hyp | Ref
| Expression |
| 1 | | simplll 775 |
. . 3
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑥 ∈ 𝐵) |
| 2 | | simpllr 776 |
. . . 4
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ 𝑅) |
| 3 | | 3oalem1.1 |
. . . . . . 7
⊢ 𝐵 ∈
Cℋ |
| 4 | | 3oalem1.2 |
. . . . . . 7
⊢ 𝐶 ∈
Cℋ |
| 5 | | 3oalem1.3 |
. . . . . . 7
⊢ 𝑅 ∈
Cℋ |
| 6 | | 3oalem1.4 |
. . . . . . 7
⊢ 𝑆 ∈
Cℋ |
| 7 | 3, 4, 5, 6 | 3oalem1 31681 |
. . . . . 6
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ))) |
| 8 | | hvaddsub12 31057 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ
𝑤)) = (𝑤 +ℎ (𝑦 −ℎ 𝑤))) |
| 9 | 8 | 3anidm23 1423 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ
𝑤)) = (𝑤 +ℎ (𝑦 −ℎ 𝑤))) |
| 10 | | hvsubid 31045 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℋ → (𝑤 −ℎ
𝑤) =
0ℎ) |
| 11 | 10 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℋ → (𝑦 +ℎ (𝑤 −ℎ
𝑤)) = (𝑦 +ℎ
0ℎ)) |
| 12 | | ax-hvaddid 31023 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℋ → (𝑦 +ℎ
0ℎ) = 𝑦) |
| 13 | 11, 12 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ
𝑤)) = 𝑦) |
| 14 | 9, 13 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑤 +ℎ (𝑦 −ℎ
𝑤)) = 𝑦) |
| 15 | 14 | ad2ant2l 746 |
. . . . . . 7
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 +ℎ (𝑦 −ℎ
𝑤)) = 𝑦) |
| 16 | 15 | adantlr 715 |
. . . . . 6
⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 +ℎ (𝑦 −ℎ
𝑤)) = 𝑦) |
| 17 | 7, 16 | syl 17 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) = 𝑦) |
| 18 | | simprlr 780 |
. . . . . 6
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑤 ∈ 𝑆) |
| 19 | | eqtr2 2761 |
. . . . . . . . . . 11
⊢ ((𝑣 = (𝑥 +ℎ 𝑦) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑣 = (𝑥 +ℎ 𝑦) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤))) |
| 21 | 20 | ad2ant2l 746 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤))) |
| 22 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → 𝑥 ∈
ℋ) |
| 23 | 22 | anim1i 615 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 ∈ ℋ ∧ 𝑤 ∈
ℋ)) |
| 24 | | hvsub4 31056 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) −ℎ
(𝑥 +ℎ
𝑤)) = ((𝑥 −ℎ 𝑥) +ℎ (𝑦 −ℎ
𝑤))) |
| 25 | 23, 24 | syldan 591 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 +ℎ 𝑦) −ℎ
(𝑥 +ℎ
𝑤)) = ((𝑥 −ℎ 𝑥) +ℎ (𝑦 −ℎ
𝑤))) |
| 26 | | hvsubid 31045 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ → (𝑥 −ℎ
𝑥) =
0ℎ) |
| 27 | 26 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 −ℎ
𝑥) =
0ℎ) |
| 28 | 27 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 −ℎ
𝑥) +ℎ
(𝑦
−ℎ 𝑤)) = (0ℎ
+ℎ (𝑦
−ℎ 𝑤))) |
| 29 | | hvsubcl 31036 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 −ℎ
𝑤) ∈
ℋ) |
| 30 | | hvaddlid 31042 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 −ℎ
𝑤) ∈ ℋ →
(0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) →
(0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤)) |
| 32 | 31 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) →
(0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤)) |
| 33 | 25, 28, 32 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 +ℎ 𝑦) −ℎ
(𝑥 +ℎ
𝑤)) = (𝑦 −ℎ 𝑤)) |
| 34 | 33 | ad2ant2rl 749 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) −ℎ
(𝑥 +ℎ
𝑤)) = (𝑦 −ℎ 𝑤)) |
| 35 | 7, 34 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = (𝑦 −ℎ 𝑤)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑧 ∈ ℋ ∧ 𝑤 ∈
ℋ)) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) → 𝑤 ∈
ℋ) |
| 38 | 37 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑥 ∈ ℋ ∧ 𝑤 ∈
ℋ)) |
| 39 | | hvsub4 31056 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ
(𝑥 +ℎ
𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ (𝑤 −ℎ
𝑤))) |
| 40 | 36, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ
(𝑥 +ℎ
𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ (𝑤 −ℎ
𝑤))) |
| 41 | 10 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 −ℎ
𝑤) =
0ℎ) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 −ℎ
𝑥) +ℎ
(𝑤
−ℎ 𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ
0ℎ)) |
| 43 | | hvsubcl 31036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑧 −ℎ
𝑥) ∈
ℋ) |
| 44 | | ax-hvaddid 31023 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 −ℎ
𝑥) ∈ ℋ →
((𝑧
−ℎ 𝑥) +ℎ 0ℎ)
= (𝑧
−ℎ 𝑥)) |
| 45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑧 −ℎ
𝑥) +ℎ
0ℎ) = (𝑧
−ℎ 𝑥)) |
| 46 | 45 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑧 −ℎ
𝑥) +ℎ
0ℎ) = (𝑧
−ℎ 𝑥)) |
| 47 | 46 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 −ℎ
𝑥) +ℎ
0ℎ) = (𝑧
−ℎ 𝑥)) |
| 48 | 40, 42, 47 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ
(𝑥 +ℎ
𝑤)) = (𝑧 −ℎ 𝑥)) |
| 49 | 48 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ
(𝑥 +ℎ
𝑤)) = (𝑧 −ℎ 𝑥)) |
| 50 | 49 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ
(𝑥 +ℎ
𝑤)) = (𝑧 −ℎ 𝑥)) |
| 51 | 7, 50 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = (𝑧 −ℎ 𝑥)) |
| 52 | 21, 35, 51 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) = (𝑧 −ℎ 𝑥)) |
| 53 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) → 𝑥 ∈ 𝐵) |
| 54 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → 𝑧 ∈ 𝐶) |
| 55 | 4 | chshii 31246 |
. . . . . . . . . . . 12
⊢ 𝐶 ∈
Sℋ |
| 56 | 3 | chshii 31246 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈
Sℋ |
| 57 | 55, 56 | shsvsi 31386 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐵) → (𝑧 −ℎ 𝑥) ∈ (𝐶 +ℋ 𝐵)) |
| 58 | 57 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑧 −ℎ 𝑥) ∈ (𝐶 +ℋ 𝐵)) |
| 59 | 56, 55 | shscomi 31382 |
. . . . . . . . . 10
⊢ (𝐵 +ℋ 𝐶) = (𝐶 +ℋ 𝐵) |
| 60 | 58, 59 | eleqtrrdi 2852 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑧 −ℎ 𝑥) ∈ (𝐵 +ℋ 𝐶)) |
| 61 | 53, 54, 60 | syl2an 596 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑧 −ℎ 𝑥) ∈ (𝐵 +ℋ 𝐶)) |
| 62 | 52, 61 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ (𝐵 +ℋ 𝐶)) |
| 63 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) → 𝑦 ∈ 𝑅) |
| 64 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → 𝑤 ∈ 𝑆) |
| 65 | 5 | chshii 31246 |
. . . . . . . . 9
⊢ 𝑅 ∈
Sℋ |
| 66 | 6 | chshii 31246 |
. . . . . . . . 9
⊢ 𝑆 ∈
Sℋ |
| 67 | 65, 66 | shsvsi 31386 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑅 ∧ 𝑤 ∈ 𝑆) → (𝑦 −ℎ 𝑤) ∈ (𝑅 +ℋ 𝑆)) |
| 68 | 63, 64, 67 | syl2an 596 |
. . . . . . 7
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ (𝑅 +ℋ 𝑆)) |
| 69 | 62, 68 | elind 4200 |
. . . . . 6
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))) |
| 70 | 56, 55 | shscli 31336 |
. . . . . . . 8
⊢ (𝐵 +ℋ 𝐶) ∈
Sℋ |
| 71 | 65, 66 | shscli 31336 |
. . . . . . . 8
⊢ (𝑅 +ℋ 𝑆) ∈
Sℋ |
| 72 | 70, 71 | shincli 31381 |
. . . . . . 7
⊢ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)) ∈
Sℋ |
| 73 | 66, 72 | shsvai 31383 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑆 ∧ (𝑦 −ℎ 𝑤) ∈ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))) |
| 74 | 18, 69, 73 | syl2anc 584 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))) |
| 75 | 17, 74 | eqeltrrd 2842 |
. . . 4
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))) |
| 76 | 2, 75 | elind 4200 |
. . 3
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) |
| 77 | 66, 72 | shscli 31336 |
. . . . 5
⊢ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))) ∈
Sℋ |
| 78 | 65, 77 | shincli 31381 |
. . . 4
⊢ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))) ∈
Sℋ |
| 79 | 56, 78 | shsvai 31383 |
. . 3
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) → (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) |
| 80 | 1, 76, 79 | syl2anc 584 |
. 2
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) |
| 81 | | eleq1 2829 |
. . 3
⊢ (𝑣 = (𝑥 +ℎ 𝑦) → (𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ↔ (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))) |
| 82 | 81 | ad2antlr 727 |
. 2
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ↔ (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))) |
| 83 | 80, 82 | mpbird 257 |
1
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) |