Step |
Hyp |
Ref |
Expression |
1 |
|
lcfl5.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
lcfl5.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
lcfl5.o |
⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
lcfl5.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
lcfl5.f |
⊢ 𝐹 = ( LFnl ‘ 𝑈 ) |
6 |
|
lcfl5.l |
⊢ 𝐿 = ( LKer ‘ 𝑈 ) |
7 |
|
lcfl5.c |
⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } |
8 |
|
lcfl5.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
9 |
|
lcfl5.g |
⊢ ( 𝜑 → 𝐺 ∈ 𝐹 ) |
10 |
7 9
|
lcfl1 |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
12 |
1 4 8
|
dvhlmod |
⊢ ( 𝜑 → 𝑈 ∈ LMod ) |
13 |
11 5 6 12 9
|
lkrssv |
⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) |
14 |
1 2 4 11 3 8 13
|
dochoccl |
⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ∈ ran 𝐼 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) ) |
15 |
10 14
|
bitr4d |
⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( 𝐿 ‘ 𝐺 ) ∈ ran 𝐼 ) ) |