Step |
Hyp |
Ref |
Expression |
1 |
|
mapdval.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
mapdval.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
mapdval.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑈 ) |
4 |
|
mapdval.f |
⊢ 𝐹 = ( LFnl ‘ 𝑈 ) |
5 |
|
mapdval.l |
⊢ 𝐿 = ( LKer ‘ 𝑈 ) |
6 |
|
mapdval.o |
⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
mapdval.m |
⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
mapdval.k |
⊢ ( 𝜑 → ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) ) |
9 |
|
mapdval.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝑆 ) |
10 |
1 2 3 4 5 6 7
|
mapdfval |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) |
11 |
8 10
|
syl |
⊢ ( 𝜑 → 𝑀 = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) |
12 |
11
|
fveq1d |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = ( ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) ) |
13 |
4
|
fvexi |
⊢ 𝐹 ∈ V |
14 |
13
|
rabex |
⊢ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ∈ V |
15 |
|
sseq2 |
⊢ ( 𝑠 = 𝑇 → ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) |
16 |
15
|
anbi2d |
⊢ ( 𝑠 = 𝑇 → ( ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) ) |
17 |
16
|
rabbidv |
⊢ ( 𝑠 = 𝑇 → { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ) |
18 |
|
eqid |
⊢ ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) |
19 |
17 18
|
fvmptg |
⊢ ( ( 𝑇 ∈ 𝑆 ∧ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ∈ V ) → ( ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ) |
20 |
9 14 19
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ) |
21 |
12 20
|
eqtrd |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ) |