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 ⊢ H = LHyp ⁡ K
dia1.t ⊢ T = LTrn ⁡ K ⁡ W
dia1.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia1N ⊢ K ∈ HL ∧ W ∈ H → I ⁡ W = T

Proof

Step Hyp Ref Expression
1 dia1.h ⊢ H = LHyp ⁡ K
2 dia1.t ⊢ T = LTrn ⁡ K ⁡ W
3 dia1.i ⊢ I = DIsoA ⁡ K ⁡ W
4 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
5 eqid ⊢ Base K = Base K
6 5 1 lhpbase ⊢ W ∈ H → W ∈ Base K
7 6 adantl ⊢ K ∈ HL ∧ W ∈ H → W ∈ Base K
8 hllat ⊢ K ∈ HL → K ∈ Lat
9 eqid ⊢ ≤ K = ≤ K
10 5 9 latref ⊢ K ∈ Lat ∧ W ∈ Base K → W ≤ K W
11 8 6 10 syl2an ⊢ K ∈ HL ∧ W ∈ H → W ≤ K W
12 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
13 5 9 1 2 12 3 diaval ⊢ K ∈ HL ∧ W ∈ H ∧ W ∈ Base K ∧ W ≤ K W → I ⁡ W = f ∈ T | trL ⁡ K ⁡ W ⁡ f ≤ K W
14 4 7 11 13 syl12anc ⊢ K ∈ HL ∧ W ∈ H → I ⁡ W = f ∈ T | trL ⁡ K ⁡ W ⁡ f ≤ K W
15 9 1 2 12 trlle ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → trL ⁡ K ⁡ W ⁡ f ≤ K W
16 15 ralrimiva ⊢ K ∈ HL ∧ W ∈ H → ∀ f ∈ T trL ⁡ K ⁡ W ⁡ f ≤ K W
17 rabid2 ⊢ T = f ∈ T | trL ⁡ K ⁡ W ⁡ f ≤ K W ↔ ∀ f ∈ T trL ⁡ K ⁡ W ⁡ f ≤ K W
18 16 17 sylibr ⊢ K ∈ HL ∧ W ∈ H → T = f ∈ T | trL ⁡ K ⁡ W ⁡ f ≤ K W
19 14 18 eqtr4d ⊢ K ∈ HL ∧ W ∈ H → I ⁡ W = T