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 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 𝑊 ) = 𝑇 )