Proof of Theorem islindeps
Step | Hyp | Ref
| Expression |
1 | | lindepsnlininds 45466 |
. . 3
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ 𝑊) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀)) |
2 | 1 | ancoms 462 |
. 2
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 ↔ ¬ 𝑆 linIndS 𝑀)) |
3 | | islindeps.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
4 | | islindeps.z |
. . . . . 6
⊢ 𝑍 = (0g‘𝑀) |
5 | | islindeps.r |
. . . . . 6
⊢ 𝑅 = (Scalar‘𝑀) |
6 | | islindeps.e |
. . . . . 6
⊢ 𝐸 = (Base‘𝑅) |
7 | | islindeps.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
8 | 3, 4, 5, 6, 7 | islininds 45460 |
. . . . 5
⊢ ((𝑆 ∈ 𝒫 𝐵 ∧ 𝑀 ∈ 𝑊) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) |
9 | 8 | ancoms 462 |
. . . 4
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linIndS 𝑀 ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) |
10 | | ibar 532 |
. . . . . 6
⊢ (𝑆 ∈ 𝒫 𝐵 → (∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ (𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )))) |
11 | 10 | bicomd 226 |
. . . . 5
⊢ (𝑆 ∈ 𝒫 𝐵 → ((𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) ↔ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) |
12 | 11 | adantl 485 |
. . . 4
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → ((𝑆 ∈ 𝒫 𝐵 ∧ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) ↔ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) |
13 | 9, 12 | bitrd 282 |
. . 3
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linIndS 𝑀 ↔ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) |
14 | 13 | notbid 321 |
. 2
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (¬ 𝑆 linIndS 𝑀 ↔ ¬ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ))) |
15 | | rexnal 3160 |
. . . 4
⊢
(∃𝑓 ∈
(𝐸 ↑m 𝑆) ¬ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ¬
∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) |
16 | | df-ne 2941 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0 ) |
17 | 16 | rexbii 3170 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑆 (𝑓‘𝑥) ≠ 0 ↔ ∃𝑥 ∈ 𝑆 ¬ (𝑓‘𝑥) = 0 ) |
18 | | rexnal 3160 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑆 ¬ (𝑓‘𝑥) = 0 ↔ ¬ ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) |
19 | 17, 18 | bitr2i 279 |
. . . . . . 7
⊢ (¬
∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ↔ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ) |
20 | 19 | anbi2i 626 |
. . . . . 6
⊢ (((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ∧ ¬ ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 )) |
21 | | pm4.61 408 |
. . . . . 6
⊢ (¬
((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ∧ ¬ ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 )) |
22 | | df-3an 1091 |
. . . . . 6
⊢ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ) ↔ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 )) |
23 | 20, 21, 22 | 3bitr4i 306 |
. . . . 5
⊢ (¬
((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ (𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 )) |
24 | 23 | rexbii 3170 |
. . . 4
⊢
(∃𝑓 ∈
(𝐸 ↑m 𝑆) ¬ ((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 )) |
25 | 15, 24 | bitr3i 280 |
. . 3
⊢ (¬
∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 )) |
26 | 25 | a1i 11 |
. 2
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (¬ ∀𝑓 ∈ (𝐸 ↑m 𝑆)((𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → ∀𝑥 ∈ 𝑆 (𝑓‘𝑥) = 0 ) ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ))) |
27 | 2, 14, 26 | 3bitrd 308 |
1
⊢ ((𝑀 ∈ 𝑊 ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑆 linDepS 𝑀 ↔ ∃𝑓 ∈ (𝐸 ↑m 𝑆)(𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍 ∧ ∃𝑥 ∈ 𝑆 (𝑓‘𝑥) ≠ 0 ))) |