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. ‘ 𝐾 )
dib0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dib0.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dib0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dib0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
Assertion dib0 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )

Proof

Step Hyp Ref Expression
1 dib0.z ⊢ 0 = ( 0. ‘ 𝐾 )
2 dib0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dib0.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
4 dib0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dib0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
6 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
7 resiexg ⊢ ( ( Base ‘ 𝐾 ) ∈ V → ( I ↾ ( Base ‘ 𝐾 ) ) ∈ V )
8 6 7 ax-mp ⊢ ( I ↾ ( Base ‘ 𝐾 ) ) ∈ V
9 fvex ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
10 9 mptex ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ V
11 8 10 xpsn ⊢ ( { ( I ↾ ( Base ‘ 𝐾 ) ) } × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) = { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ }
12 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
14 13 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
15 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 1 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
17 14 16 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
18 15 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
19 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
20 15 19 1 op0le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑊 )
21 13 18 20 syl2an ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ( le ‘ 𝐾 ) 𝑊 )
22 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
23 eqid ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
24 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
25 15 19 2 22 23 24 3 dibval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 0 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 0 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
26 12 17 21 25 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
27 15 1 2 24 dia0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) = { ( I ↾ ( Base ‘ 𝐾 ) ) } )
28 27 xpeq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) = ( { ( I ↾ ( Base ‘ 𝐾 ) ) } × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
29 26 28 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = ( { ( I ↾ ( Base ‘ 𝐾 ) ) } × { ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
30 15 2 22 4 5 23 dvh0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ )
31 30 sneqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 𝑂 } = { ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ⟩ } )
32 11 29 31 3eqtr4a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )