Metamath Proof Explorer

Theorem dva0g

Description: The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014)

Ref Expression
Hypotheses dva0g.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dva0g.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dva0g.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dva0g.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dva0g.z ⊢ 0 = ( 0g ‘ 𝑈 )
Assertion dva0g ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ( I ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dva0g.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dva0g.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dva0g.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dva0g.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
5 dva0g.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 1 2 3 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
8 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
9 2 3 4 8 dvavadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ ( I ↾ 𝐵 ) ∈ 𝑇 ) ) → ( ( I ↾ 𝐵 ) ( +g ‘ 𝑈 ) ( I ↾ 𝐵 ) ) = ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) )
10 6 7 7 9 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝐵 ) ( +g ‘ 𝑈 ) ( I ↾ 𝐵 ) ) = ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) )
11 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
12 f1of ⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
13 fcoi2 ⊢ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
14 11 12 13 mp2b ⊢ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 )
15 10 14 eqtrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝐵 ) ( +g ‘ 𝑈 ) ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
16 2 4 dvalvec ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )
17 lveclmod ⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
18 16 17 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod )
19 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20 2 3 4 19 dvavbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = 𝑇 )
21 7 20 eleqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ ( Base ‘ 𝑈 ) )
22 19 8 5 lmod0vid ⊢ ( ( 𝑈 ∈ LMod ∧ ( I ↾ 𝐵 ) ∈ ( Base ‘ 𝑈 ) ) → ( ( ( I ↾ 𝐵 ) ( +g ‘ 𝑈 ) ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) ↔ 0 = ( I ↾ 𝐵 ) ) )
23 18 21 22 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( I ↾ 𝐵 ) ( +g ‘ 𝑈 ) ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) ↔ 0 = ( I ↾ 𝐵 ) ) )
24 15 23 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ( I ↾ 𝐵 ) )