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 |
|
mapdvalc.c |
⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) } |
11 |
1 2 3 4 5 6 7 8 9
|
mapdval |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } ) |
12 |
|
anass |
⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) ) |
13 |
10
|
lcfl1lem |
⊢ ( 𝑓 ∈ 𝐶 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ) |
14 |
13
|
anbi1i |
⊢ ( ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ↔ ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) |
15 |
14
|
bicomi |
⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) |
16 |
15
|
a1i |
⊢ ( 𝜑 → ( ( ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ↔ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) ) |
17 |
12 16
|
bitr3id |
⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐹 ∧ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) ↔ ( 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) ) ) |
18 |
17
|
rabbidva2 |
⊢ ( 𝜑 → { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } ) |
19 |
11 18
|
eqtrd |
⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 } ) |