This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dih0

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

Ref Expression
Hypotheses dih0.z ⊢ 0 = ( 0. ‘ 𝐾 )
dih0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dih0.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dih0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dih0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
Assertion dih0 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )

Proof

Step Hyp Ref Expression
1 dih0.z ⊢ 0 = ( 0. ‘ 𝐾 )
2 dih0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dih0.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dih0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dih0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
6 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 7 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 1 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
11 8 10 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
12 9 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14 9 13 1 op0le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑊 )
15 7 12 14 syl2an ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ( le ‘ 𝐾 ) 𝑊 )
16 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
17 9 13 2 3 16 dihvalb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 0 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 0 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) )
18 6 11 15 17 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) )
19 1 2 16 4 5 dib0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) = { 𝑂 } )
20 18 19 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )