This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dia1N

Description: The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia1.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dia1N ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) = 𝑇 )

Proof

Step Hyp Ref Expression
1 dia1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dia1.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 1 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
7 6 adantl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
10 5 9 latref ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
11 8 6 10 syl2an ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 )
12 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 5 9 1 2 12 3 diaval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 𝑊 ) = { 𝑓 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 } )
14 4 7 11 13 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) = { 𝑓 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 } )
15 9 1 2 12 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 )
16 15 ralrimiva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 )
17 rabid2 ⊢ ( 𝑇 = { 𝑓 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 } ↔ ∀ 𝑓 ∈ 𝑇 ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 )
18 16 17 sylibr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑇 = { 𝑓 ∈ 𝑇 ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) 𝑊 } )
19 14 18 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) = 𝑇 )