| Step | Hyp | Ref
| Expression |
| 1 | | neq0 4352 |
. . 3
⊢ (¬
(𝐴 ∖ 𝐵) = ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 2 | | ssdif0 4366 |
. . 3
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∖ 𝐵) = ∅) |
| 3 | 1, 2 | xchnxbir 333 |
. 2
⊢ (¬
𝐴 ⊆ 𝐵 ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 4 | | eldifi 4131 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴) |
| 5 | | strlem1.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Cℋ |
| 6 | 5 | cheli 31251 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ) |
| 7 | | normcl 31144 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
| 8 | 4, 6, 7 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(normℎ‘𝑥) ∈ ℝ) |
| 9 | | strlem1.2 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ∈
Cℋ |
| 10 | | ch0 31247 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈
Cℋ → 0ℎ ∈ 𝐵) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
0ℎ ∈ 𝐵 |
| 12 | | eldifn 4132 |
. . . . . . . . . . . . . . 15
⊢
(0ℎ ∈ (𝐴 ∖ 𝐵) → ¬ 0ℎ ∈
𝐵) |
| 13 | 11, 12 | mt2 200 |
. . . . . . . . . . . . . 14
⊢ ¬
0ℎ ∈ (𝐴 ∖ 𝐵) |
| 14 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0ℎ →
(𝑥 ∈ (𝐴 ∖ 𝐵) ↔ 0ℎ ∈ (𝐴 ∖ 𝐵))) |
| 15 | 13, 14 | mtbiri 327 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0ℎ →
¬ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
| 16 | 15 | con2i 139 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬ 𝑥 = 0ℎ) |
| 17 | | norm-i 31148 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
| 18 | 4, 6, 17 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
| 19 | 16, 18 | mtbird 325 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ¬
(normℎ‘𝑥) = 0) |
| 20 | 19 | neqned 2947 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(normℎ‘𝑥) ≠ 0) |
| 21 | 8, 20 | rereccld 12094 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (1 /
(normℎ‘𝑥)) ∈ ℝ) |
| 22 | 21 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (1 /
(normℎ‘𝑥)) ∈ ℂ) |
| 23 | 5 | chshii 31246 |
. . . . . . . . . 10
⊢ 𝐴 ∈
Sℋ |
| 24 | | shmulcl 31237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
Sℋ ∧ (1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝐴) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴) |
| 25 | 23, 24 | mp3an1 1450 |
. . . . . . . . 9
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ 𝐴) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴) |
| 26 | 25 | ex 412 |
. . . . . . . 8
⊢ ((1 /
(normℎ‘𝑥)) ∈ ℂ → (𝑥 ∈ 𝐴 → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴)) |
| 27 | 22, 26 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝑥 ∈ 𝐴 → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴)) |
| 28 | 8 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(normℎ‘𝑥) ∈ ℂ) |
| 29 | 9 | chshii 31246 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈
Sℋ |
| 30 | | shmulcl 31237 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
Sℋ ∧ (normℎ‘𝑥) ∈ ℂ ∧ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵) →
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ 𝐵) |
| 31 | 29, 30 | mp3an1 1450 |
. . . . . . . . . . 11
⊢
(((normℎ‘𝑥) ∈ ℂ ∧ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵) →
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ 𝐵) |
| 32 | 31 | ex 412 |
. . . . . . . . . 10
⊢
((normℎ‘𝑥) ∈ ℂ → (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵 →
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ 𝐵)) |
| 33 | 28, 32 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵 →
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ 𝐵)) |
| 34 | 28, 20 | recidd 12038 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
((normℎ‘𝑥) · (1 /
(normℎ‘𝑥))) = 1) |
| 35 | 34 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(((normℎ‘𝑥) · (1 /
(normℎ‘𝑥))) ·ℎ 𝑥) = (1
·ℎ 𝑥)) |
| 36 | 4, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ ℋ) |
| 37 | | ax-hvmulass 31026 |
. . . . . . . . . . . 12
⊢
(((normℎ‘𝑥) ∈ ℂ ∧ (1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(((normℎ‘𝑥) · (1 /
(normℎ‘𝑥))) ·ℎ 𝑥) =
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
| 38 | 28, 22, 36, 37 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(((normℎ‘𝑥) · (1 /
(normℎ‘𝑥))) ·ℎ 𝑥) =
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
| 39 | | ax-hvmulid 31025 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℋ → (1
·ℎ 𝑥) = 𝑥) |
| 40 | 4, 6, 39 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (1
·ℎ 𝑥) = 𝑥) |
| 41 | 35, 38, 40 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = 𝑥) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) →
(((normℎ‘𝑥) ·ℎ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ 𝐵 ↔ 𝑥 ∈ 𝐵)) |
| 43 | 33, 42 | sylibd 239 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵 → 𝑥 ∈ 𝐵)) |
| 44 | 43 | con3d 152 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (¬ 𝑥 ∈ 𝐵 → ¬ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵)) |
| 45 | 27, 44 | anim12d 609 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) → (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴 ∧ ¬ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵))) |
| 46 | | eldif 3961 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
| 47 | | eldif 3961 |
. . . . . 6
⊢ (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ (𝐴 ∖ 𝐵) ↔ (((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐴 ∧ ¬ ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ 𝐵)) |
| 48 | 45, 46, 47 | 3imtr4g 296 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝑥 ∈ (𝐴 ∖ 𝐵) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ (𝐴 ∖ 𝐵))) |
| 49 | 48 | pm2.43i 52 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ (𝐴 ∖ 𝐵)) |
| 50 | | norm-iii 31159 |
. . . . . 6
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = ((abs‘(1 /
(normℎ‘𝑥))) ·
(normℎ‘𝑥))) |
| 51 | 22, 36, 50 | syl2anc 584 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ 𝑥)) = ((abs‘(1 /
(normℎ‘𝑥))) ·
(normℎ‘𝑥))) |
| 52 | 15 | necon2ai 2970 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ≠ 0ℎ) |
| 53 | | normgt0 31146 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℋ → (𝑥 ≠ 0ℎ
↔ 0 < (normℎ‘𝑥))) |
| 54 | 4, 6, 53 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (𝑥 ≠ 0ℎ ↔ 0 <
(normℎ‘𝑥))) |
| 55 | 52, 54 | mpbid 232 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 0 <
(normℎ‘𝑥)) |
| 56 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 57 | | 0le1 11786 |
. . . . . . . . 9
⊢ 0 ≤
1 |
| 58 | | divge0 12137 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ ((normℎ‘𝑥) ∈ ℝ ∧ 0 <
(normℎ‘𝑥))) → 0 ≤ (1 /
(normℎ‘𝑥))) |
| 59 | 56, 57, 58 | mpanl12 702 |
. . . . . . . 8
⊢
(((normℎ‘𝑥) ∈ ℝ ∧ 0 <
(normℎ‘𝑥)) → 0 ≤ (1 /
(normℎ‘𝑥))) |
| 60 | 8, 55, 59 | syl2anc 584 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 0 ≤ (1 /
(normℎ‘𝑥))) |
| 61 | 21, 60 | absidd 15461 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (abs‘(1 /
(normℎ‘𝑥))) = (1 /
(normℎ‘𝑥))) |
| 62 | 61 | oveq1d 7446 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ((abs‘(1 /
(normℎ‘𝑥))) ·
(normℎ‘𝑥)) = ((1 /
(normℎ‘𝑥)) ·
(normℎ‘𝑥))) |
| 63 | 28, 20 | recid2d 12039 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ((1 /
(normℎ‘𝑥)) ·
(normℎ‘𝑥)) = 1) |
| 64 | 51, 62, 63 | 3eqtrd 2781 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ 𝑥)) = 1) |
| 65 | | fveqeq2 6915 |
. . . . 5
⊢ (𝑢 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
((normℎ‘𝑢) = 1 ↔
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = 1)) |
| 66 | 65 | rspcev 3622 |
. . . 4
⊢ ((((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = 1) → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1) |
| 67 | 49, 64, 66 | syl2anc 584 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1) |
| 68 | 67 | exlimiv 1930 |
. 2
⊢
(∃𝑥 𝑥 ∈ (𝐴 ∖ 𝐵) → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1) |
| 69 | 3, 68 | sylbi 217 |
1
⊢ (¬
𝐴 ⊆ 𝐵 → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1) |