Step |
Hyp |
Ref |
Expression |
1 |
|
dih1dimb2.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
dih1dimb2.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
dih1dimb2.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
dih1dimb2.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
5 |
|
dih1dimb2.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
dih1dimb2.o |
⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) |
7 |
|
dih1dimb2.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
dih1dimb2.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
|
dih1dimb2.n |
⊢ 𝑁 = ( LSpan ‘ 𝑈 ) |
10 |
|
eqid |
⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
11 |
2 3 4 5 10
|
cdlemf |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) |
12 |
|
simp3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) |
13 |
|
simp1rl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑄 ∈ 𝐴 ) |
14 |
12 13
|
eqeltrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) |
15 |
|
simp1l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
16 |
|
simp2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓 ∈ 𝑇 ) |
17 |
1 3 4 5 10
|
trlnidatb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) ) |
18 |
15 16 17
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ 𝐴 ) ) |
19 |
14 18
|
mpbird |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → 𝑓 ≠ ( I ↾ 𝐵 ) ) |
20 |
12
|
fveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝐼 ‘ 𝑄 ) ) |
21 |
1 4 5 10 6 7 8 9
|
dih1dimb |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) |
22 |
15 16 21
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) |
23 |
20 22
|
eqtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) |
24 |
19 23
|
jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) ) |
25 |
24
|
3expia |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) ) ) |
26 |
25
|
reximdva |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) = 𝑄 → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) ) ) |
27 |
11 26
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { 〈 𝑓 , 𝑂 〉 } ) ) ) |