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=BaseK
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=BaseK
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˙≤KW
13 6 10 12 syl2an ⊢K∈HL∧W∈H→0˙≤KW
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˙≤KW→I⁡0˙=f∈LTrn⁡K⁡W|trL⁡K⁡W⁡f≤K0˙
17 5 9 13 16 syl12anc ⊢K∈HL∧W∈H→I⁡0˙=f∈LTrn⁡K⁡W|trL⁡K⁡W⁡f≤K0˙
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≤K0˙↔trL⁡K⁡W⁡f=0˙
21 18 19 20 syl2anc ⊢K∈HL∧W∈H∧f∈LTrn⁡K⁡W→trL⁡K⁡W⁡f≤K0˙↔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≤K0˙↔f=I↾B
24 23 rabbidva ⊢K∈HL∧W∈H→f∈LTrn⁡K⁡W|trL⁡K⁡W⁡f≤K0˙=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