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 ) = { 𝑂 } )