Metamath Proof Explorer

Theorem dib0

Description: The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014)

Ref Expression
Hypotheses dib0.z ⊢0˙=0.⁡K
dib0.h ⊢H=LHyp⁡K
dib0.i ⊢I=DIsoB⁡K⁡W
dib0.u ⊢U=DVecH⁡K⁡W
dib0.o ⊢O=0U
Assertion dib0 ⊢K∈HL∧W∈H→I⁡0˙=O

Proof

Step Hyp Ref Expression
1 dib0.z ⊢0˙=0.⁡K
2 dib0.h ⊢H=LHyp⁡K
3 dib0.i ⊢I=DIsoB⁡K⁡W
4 dib0.u ⊢U=DVecH⁡K⁡W
5 dib0.o ⊢O=0U
6 fvex ⊢BaseK∈V
7 resiexg ⊢BaseK∈V→I↾BaseK∈V
8 6 7 ax-mp ⊢I↾BaseK∈V
9 fvex ⊢LTrn⁡K⁡W∈V
10 9 mptex ⊢f∈LTrn⁡K⁡W⟼I↾BaseK∈V
11 8 10 xpsn ⊢I↾BaseK×f∈LTrn⁡K⁡W⟼I↾BaseK=I↾BaseKf∈LTrn⁡K⁡W⟼I↾BaseK
12 id ⊢K∈HL∧W∈H→K∈HL∧W∈H
13 hlop ⊢K∈HL→K∈OP
14 13 adantr ⊢K∈HL∧W∈H→K∈OP
15 eqid ⊢BaseK=BaseK
16 15 1 op0cl ⊢K∈OP→0˙∈BaseK
17 14 16 syl ⊢K∈HL∧W∈H→0˙∈BaseK
18 15 2 lhpbase ⊢W∈H→W∈BaseK
19 eqid ⊢≤K=≤K
20 15 19 1 op0le ⊢K∈OP∧W∈BaseK→0˙≤KW
21 13 18 20 syl2an ⊢K∈HL∧W∈H→0˙≤KW
22 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
23 eqid ⊢f∈LTrn⁡K⁡W⟼I↾BaseK=f∈LTrn⁡K⁡W⟼I↾BaseK
24 eqid ⊢DIsoA⁡K⁡W=DIsoA⁡K⁡W
25 15 19 2 22 23 24 3 dibval2 ⊢K∈HL∧W∈H∧0˙∈BaseK∧0˙≤KW→I⁡0˙=DIsoA⁡K⁡W⁡0˙×f∈LTrn⁡K⁡W⟼I↾BaseK
26 12 17 21 25 syl12anc ⊢K∈HL∧W∈H→I⁡0˙=DIsoA⁡K⁡W⁡0˙×f∈LTrn⁡K⁡W⟼I↾BaseK
27 15 1 2 24 dia0 ⊢K∈HL∧W∈H→DIsoA⁡K⁡W⁡0˙=I↾BaseK
28 27 xpeq1d ⊢K∈HL∧W∈H→DIsoA⁡K⁡W⁡0˙×f∈LTrn⁡K⁡W⟼I↾BaseK=I↾BaseK×f∈LTrn⁡K⁡W⟼I↾BaseK
29 26 28 eqtrd ⊢K∈HL∧W∈H→I⁡0˙=I↾BaseK×f∈LTrn⁡K⁡W⟼I↾BaseK
30 15 2 22 4 5 23 dvh0g ⊢K∈HL∧W∈H→O=I↾BaseKf∈LTrn⁡K⁡W⟼I↾BaseK
31 30 sneqd ⊢K∈HL∧W∈H→O=I↾BaseKf∈LTrn⁡K⁡W⟼I↾BaseK
32 11 29 31 3eqtr4a ⊢K∈HL∧W∈H→I⁡0˙=O