Metamath Proof Explorer

Theorem dia0

Description: The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses dia0.b ⊢ B = Base K
dia0.z ⊢ 0 ˙ = 0. ⁡ K
dia0.h ⊢ H = LHyp ⁡ K
dia0.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion dia0 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = I ↾ B

Proof

Step Hyp Ref Expression
1 dia0.b ⊢ B = Base K
2 dia0.z ⊢ 0 ˙ = 0. ⁡ K
3 dia0.h ⊢ H = LHyp ⁡ K
4 dia0.i ⊢ I = DIsoA ⁡ K ⁡ W
5 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
6 hlatl ⊢ K ∈ HL → K ∈ AtLat
7 1 2 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ B
8 6 7 syl ⊢ K ∈ HL → 0 ˙ ∈ B
9 8 adantr ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ B
10 1 3 lhpbase ⊢ W ∈ H → W ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 atl0le ⊢ K ∈ AtLat ∧ W ∈ B → 0 ˙ ≤ K W
13 6 10 12 syl2an ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ≤ K W
14 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
15 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
16 1 11 3 14 15 4 diaval ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ B ∧ 0 ˙ ≤ K W → I ⁡ 0 ˙ = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙
17 5 9 13 16 syl12anc ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙
18 6 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W → K ∈ AtLat
19 1 3 14 15 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ f ∈ B
20 1 11 2 atlle0 ⊢ K ∈ AtLat ∧ trL ⁡ K ⁡ W ⁡ f ∈ B → trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙ ↔ trL ⁡ K ⁡ W ⁡ f = 0 ˙
21 18 19 20 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙ ↔ trL ⁡ K ⁡ W ⁡ f = 0 ˙
22 1 2 3 14 15 trlid0b ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W → f = I ↾ B ↔ trL ⁡ K ⁡ W ⁡ f = 0 ˙
23 21 22 bitr4d ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W → trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙ ↔ f = I ↾ B
24 23 rabbidva ⊢ K ∈ HL ∧ W ∈ H → f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ K 0 ˙ = f ∈ LTrn ⁡ K ⁡ W | f = I ↾ B
25 1 3 14 idltrn ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∈ LTrn ⁡ K ⁡ W
26 rabsn ⊢ I ↾ B ∈ LTrn ⁡ K ⁡ W → f ∈ LTrn ⁡ K ⁡ W | f = I ↾ B = I ↾ B
27 25 26 syl ⊢ K ∈ HL ∧ W ∈ H → f ∈ LTrn ⁡ K ⁡ W | f = I ↾ B = I ↾ B
28 17 24 27 3eqtrd ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = I ↾ B