Step |
Hyp |
Ref |
Expression |
1 |
|
islindf.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
islindf.v |
⊢ · = ( ·𝑠 ‘ 𝑊 ) |
3 |
|
islindf.k |
⊢ 𝐾 = ( LSpan ‘ 𝑊 ) |
4 |
|
islindf.s |
⊢ 𝑆 = ( Scalar ‘ 𝑊 ) |
5 |
|
islindf.n |
⊢ 𝑁 = ( Base ‘ 𝑆 ) |
6 |
|
islindf.z |
⊢ 0 = ( 0g ‘ 𝑆 ) |
7 |
1
|
islinds |
⊢ ( 𝑊 ∈ 𝑌 → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ) ) |
8 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
9 |
8
|
ssex |
⊢ ( 𝐹 ⊆ 𝐵 → 𝐹 ∈ V ) |
10 |
9
|
adantl |
⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → 𝐹 ∈ V ) |
11 |
|
resiexg |
⊢ ( 𝐹 ∈ V → ( I ↾ 𝐹 ) ∈ V ) |
12 |
10 11
|
syl |
⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) ∈ V ) |
13 |
1 2 3 4 5 6
|
islindf |
⊢ ( ( 𝑊 ∈ 𝑌 ∧ ( I ↾ 𝐹 ) ∈ V ) → ( ( I ↾ 𝐹 ) LIndF 𝑊 ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ) |
14 |
12 13
|
syldan |
⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → ( ( I ↾ 𝐹 ) LIndF 𝑊 ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ) |
15 |
14
|
pm5.32da |
⊢ ( 𝑊 ∈ 𝑌 → ( ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ) ) |
16 |
|
dmresi |
⊢ dom ( I ↾ 𝐹 ) = 𝐹 |
17 |
16
|
raleqi |
⊢ ( ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) |
18 |
|
fvresi |
⊢ ( 𝑥 ∈ 𝐹 → ( ( I ↾ 𝐹 ) ‘ 𝑥 ) = 𝑥 ) |
19 |
18
|
oveq2d |
⊢ ( 𝑥 ∈ 𝐹 → ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑘 · 𝑥 ) ) |
20 |
16
|
difeq1i |
⊢ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) = ( 𝐹 ∖ { 𝑥 } ) |
21 |
20
|
imaeq2i |
⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) = ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) ) |
22 |
|
difss |
⊢ ( 𝐹 ∖ { 𝑥 } ) ⊆ 𝐹 |
23 |
|
resiima |
⊢ ( ( 𝐹 ∖ { 𝑥 } ) ⊆ 𝐹 → ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } ) ) |
24 |
22 23
|
ax-mp |
⊢ ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } ) |
25 |
21 24
|
eqtri |
⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } ) |
26 |
25
|
fveq2i |
⊢ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) |
27 |
26
|
a1i |
⊢ ( 𝑥 ∈ 𝐹 → ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) |
28 |
19 27
|
eleq12d |
⊢ ( 𝑥 ∈ 𝐹 → ( ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
29 |
28
|
notbid |
⊢ ( 𝑥 ∈ 𝐹 → ( ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
30 |
29
|
ralbidv |
⊢ ( 𝑥 ∈ 𝐹 → ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
31 |
30
|
ralbiia |
⊢ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) |
32 |
17 31
|
bitri |
⊢ ( ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) |
33 |
32
|
anbi2i |
⊢ ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
34 |
|
f1oi |
⊢ ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 |
35 |
|
f1of |
⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 ) |
36 |
34 35
|
ax-mp |
⊢ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 |
37 |
16
|
feq2i |
⊢ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 ↔ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 ) |
38 |
36 37
|
mpbir |
⊢ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 |
39 |
|
fss |
⊢ ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ) |
40 |
38 39
|
mpan |
⊢ ( 𝐹 ⊆ 𝐵 → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ) |
41 |
40
|
biantrurd |
⊢ ( 𝐹 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) ) |
42 |
33 41
|
bitr4id |
⊢ ( 𝐹 ⊆ 𝐵 → ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
43 |
42
|
pm5.32i |
⊢ ( ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) |
44 |
43
|
a1i |
⊢ ( 𝑊 ∈ 𝑌 → ( ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) ) |
45 |
7 15 44
|
3bitrd |
⊢ ( 𝑊 ∈ 𝑌 → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) ) |