| Step | Hyp | Ref
| Expression |
| 1 | | elin 3967 |
. . 3
⊢ (𝑧 ∈ ((𝐴 +ℋ 𝐵) ∩ 𝐶) ↔ (𝑧 ∈ (𝐴 +ℋ 𝐵) ∧ 𝑧 ∈ 𝐶)) |
| 2 | | shmod.1 |
. . . . . . 7
⊢ 𝐴 ∈
Sℋ |
| 3 | | shmod.2 |
. . . . . . 7
⊢ 𝐵 ∈
Sℋ |
| 4 | 2, 3 | shseli 31335 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 +ℎ 𝑦)) |
| 5 | | shmod.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 ∈
Sℋ |
| 6 | 5 | sheli 31233 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ) |
| 7 | 2 | sheli 31233 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ) |
| 8 | 3 | sheli 31233 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ) |
| 9 | | hvsubadd 31096 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑧 −ℎ
𝑥) = 𝑦 ↔ (𝑥 +ℎ 𝑦) = 𝑧)) |
| 10 | 6, 7, 8, 9 | syl3an 1161 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑧 −ℎ 𝑥) = 𝑦 ↔ (𝑥 +ℎ 𝑦) = 𝑧)) |
| 11 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ ((𝑥 +ℎ 𝑦) = 𝑧 ↔ 𝑧 = (𝑥 +ℎ 𝑦)) |
| 12 | 10, 11 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ((𝑧 −ℎ 𝑥) = 𝑦 ↔ 𝑧 = (𝑥 +ℎ 𝑦))) |
| 13 | 12 | 3expb 1121 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 −ℎ 𝑥) = 𝑦 ↔ 𝑧 = (𝑥 +ℎ 𝑦))) |
| 14 | 5, 2 | shsvsi 31386 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 −ℎ 𝑥) ∈ (𝐶 +ℋ 𝐴)) |
| 15 | 5, 2 | shscomi 31382 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐶 +ℋ 𝐴) = (𝐴 +ℋ 𝐶) |
| 16 | 14, 15 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 −ℎ 𝑥) ∈ (𝐴 +ℋ 𝐶)) |
| 17 | 2, 5 | shlesb1i 31405 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ⊆ 𝐶 ↔ (𝐴 +ℋ 𝐶) = 𝐶) |
| 18 | 17 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆ 𝐶 → (𝐴 +ℋ 𝐶) = 𝐶) |
| 19 | 18 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ⊆ 𝐶 → ((𝑧 −ℎ 𝑥) ∈ (𝐴 +ℋ 𝐶) ↔ (𝑧 −ℎ 𝑥) ∈ 𝐶)) |
| 20 | 16, 19 | imbitrid 244 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ⊆ 𝐶 → ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑧 −ℎ 𝑥) ∈ 𝐶)) |
| 21 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 −ℎ
𝑥) = 𝑦 → ((𝑧 −ℎ 𝑥) ∈ 𝐶 ↔ 𝑦 ∈ 𝐶)) |
| 22 | 21 | biimpd 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 −ℎ
𝑥) = 𝑦 → ((𝑧 −ℎ 𝑥) ∈ 𝐶 → 𝑦 ∈ 𝐶)) |
| 23 | 20, 22 | sylan9 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝑧 −ℎ 𝑥) = 𝑦) → ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐶)) |
| 24 | 23 | anim2d 612 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝑧 −ℎ 𝑥) = 𝑦) → ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴)) → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
| 25 | | elin 3967 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
| 26 | 24, 25 | imbitrrdi 252 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ 𝐶 ∧ (𝑧 −ℎ 𝑥) = 𝑦) → ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ (𝐵 ∩ 𝐶))) |
| 27 | 26 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ 𝐶 → ((𝑧 −ℎ 𝑥) = 𝑦 → ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴)) → 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
| 28 | 27 | com13 88 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴)) → ((𝑧 −ℎ 𝑥) = 𝑦 → (𝐴 ⊆ 𝐶 → 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
| 29 | 28 | ancoms 458 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ((𝑧 −ℎ 𝑥) = 𝑦 → (𝐴 ⊆ 𝐶 → 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
| 30 | 29 | anasss 466 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝑧 −ℎ 𝑥) = 𝑦 → (𝐴 ⊆ 𝐶 → 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
| 31 | 13, 30 | sylbird 260 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = (𝑥 +ℎ 𝑦) → (𝐴 ⊆ 𝐶 → 𝑦 ∈ (𝐵 ∩ 𝐶)))) |
| 32 | 31 | imp 406 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 = (𝑥 +ℎ 𝑦)) → (𝐴 ⊆ 𝐶 → 𝑦 ∈ (𝐵 ∩ 𝐶))) |
| 33 | 3, 5 | shincli 31381 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∩ 𝐶) ∈
Sℋ |
| 34 | 2, 33 | shsvai 31383 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → (𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))) |
| 35 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑥 +ℎ 𝑦) → (𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)) ↔ (𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 36 | 34, 35 | imbitrrid 246 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑥 +ℎ 𝑦) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐵 ∩ 𝐶)) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 37 | 36 | expd 415 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 +ℎ 𝑦) → (𝑥 ∈ 𝐴 → (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 38 | 37 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (𝑧 = (𝑥 +ℎ 𝑦) → (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 39 | 38 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = (𝑥 +ℎ 𝑦) → (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 40 | 39 | imp 406 |
. . . . . . . . 9
⊢ (((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 = (𝑥 +ℎ 𝑦)) → (𝑦 ∈ (𝐵 ∩ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 41 | 32, 40 | syld 47 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 = (𝑥 +ℎ 𝑦)) → (𝐴 ⊆ 𝐶 → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 42 | 41 | exp31 419 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 = (𝑥 +ℎ 𝑦) → (𝐴 ⊆ 𝐶 → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))))) |
| 43 | 42 | rexlimdvv 3212 |
. . . . . 6
⊢ (𝑧 ∈ 𝐶 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 +ℎ 𝑦) → (𝐴 ⊆ 𝐶 → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 44 | 4, 43 | biimtrid 242 |
. . . . 5
⊢ (𝑧 ∈ 𝐶 → (𝑧 ∈ (𝐴 +ℋ 𝐵) → (𝐴 ⊆ 𝐶 → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 45 | 44 | com13 88 |
. . . 4
⊢ (𝐴 ⊆ 𝐶 → (𝑧 ∈ (𝐴 +ℋ 𝐵) → (𝑧 ∈ 𝐶 → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶))))) |
| 46 | 45 | impd 410 |
. . 3
⊢ (𝐴 ⊆ 𝐶 → ((𝑧 ∈ (𝐴 +ℋ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 47 | 1, 46 | biimtrid 242 |
. 2
⊢ (𝐴 ⊆ 𝐶 → (𝑧 ∈ ((𝐴 +ℋ 𝐵) ∩ 𝐶) → 𝑧 ∈ (𝐴 +ℋ (𝐵 ∩ 𝐶)))) |
| 48 | 47 | ssrdv 3989 |
1
⊢ (𝐴 ⊆ 𝐶 → ((𝐴 +ℋ 𝐵) ∩ 𝐶) ⊆ (𝐴 +ℋ (𝐵 ∩ 𝐶))) |