Metamath Proof Explorer

Theorem dihwN

Description: Value of isomorphism H at the fiducial hyperplane W . (Contributed by NM, 25-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihw.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihw.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihw.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihw.o ⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihw.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihw.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion dihwN ( 𝜑 → ( 𝐼 ‘ 𝑊 ) = ( 𝑇 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 dihw.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihw.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihw.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dihw.o ⊢ 0 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
5 dihw.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dihw.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 6 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
8 1 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
9 7 8 syl ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
10 6 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
11 10 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
12 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13 1 12 latref ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
14 11 9 13 syl2anc ⊢ ( 𝜑 → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
15 9 14 jca ⊢ ( 𝜑 → ( 𝑊 ∈ 𝐵 ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) )
16 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
17 1 12 2 5 16 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑊 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) )
18 6 15 17 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑊 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) )
19 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
20 1 12 2 3 4 19 16 dibval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) × { 0 } ) )
21 6 15 20 syl2anc ⊢ ( 𝜑 → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) × { 0 } ) )
22 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
23 1 12 2 3 22 19 diaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑊 ∈ 𝐵 ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) = { 𝑔 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 } )
24 6 15 23 syl2anc ⊢ ( 𝜑 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) = { 𝑔 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 } )
25 12 2 3 22 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 )
26 6 25 sylan ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 )
27 26 ralrimiva ⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 )
28 rabid2 ⊢ ( 𝑇 = { 𝑔 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 } ↔ ∀ 𝑔 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 )
29 27 28 sylibr ⊢ ( 𝜑 → 𝑇 = { 𝑔 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) ( le ‘ 𝐾 ) 𝑊 } )
30 24 29 eqtr4d ⊢ ( 𝜑 → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) = 𝑇 )
31 30 xpeq1d ⊢ ( 𝜑 → ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑊 ) × { 0 } ) = ( 𝑇 × { 0 } ) )
32 18 21 31 3eqtrd ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑊 ) = ( 𝑇 × { 0 } ) )