Metamath Proof Explorer

Theorem hlhilphllem

Description: Lemma for hlhil . (Contributed by NM, 23-Jun-2015)

Ref Expression
Hypotheses hlhilphl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hlhilphllem.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhilphl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hlhilphllem.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
hlhilphllem.l ⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hlhilphllem.v ⊢ 𝑉 = ( Base ‘ 𝐿 )
hlhilphllem.a ⊢ + = ( +g ‘ 𝐿 )
hlhilphllem.s ⊢ · = ( ·𝑠 ‘ 𝐿 )
hlhilphllem.r ⊢ 𝑅 = ( Scalar ‘ 𝐿 )
hlhilphllem.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hlhilphllem.p ⊢ ⨣ = ( +g ‘ 𝑅 )
hlhilphllem.t ⊢ × = ( .r ‘ 𝑅 )
hlhilphllem.q ⊢ 𝑄 = ( 0g ‘ 𝑅 )
hlhilphllem.z ⊢ 0 = ( 0g ‘ 𝐿 )
hlhilphllem.i ⊢ , = ( ·𝑖 ‘ 𝑈 )
hlhilphllem.j ⊢ 𝐽 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hlhilphllem.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hlhilphllem.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝐽 ‘ 𝑦 ) ‘ 𝑥 ) )
Assertion hlhilphllem ( 𝜑 → 𝑈 ∈ PreHil )

Proof

Step Hyp Ref Expression
1 hlhilphl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhilphllem.u ⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
3 hlhilphl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4 hlhilphllem.f ⊢ 𝐹 = ( Scalar ‘ 𝑈 )
5 hlhilphllem.l ⊢ 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 hlhilphllem.v ⊢ 𝑉 = ( Base ‘ 𝐿 )
7 hlhilphllem.a ⊢ + = ( +g ‘ 𝐿 )
8 hlhilphllem.s ⊢ · = ( ·𝑠 ‘ 𝐿 )
9 hlhilphllem.r ⊢ 𝑅 = ( Scalar ‘ 𝐿 )
10 hlhilphllem.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
11 hlhilphllem.p ⊢ ⨣ = ( +g ‘ 𝑅 )
12 hlhilphllem.t ⊢ × = ( .r ‘ 𝑅 )
13 hlhilphllem.q ⊢ 𝑄 = ( 0g ‘ 𝑅 )
14 hlhilphllem.z ⊢ 0 = ( 0g ‘ 𝐿 )
15 hlhilphllem.i ⊢ , = ( ·𝑖 ‘ 𝑈 )
16 hlhilphllem.j ⊢ 𝐽 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
17 hlhilphllem.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
18 hlhilphllem.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝐽 ‘ 𝑦 ) ‘ 𝑥 ) )
19 1 2 3 5 6 hlhilbase ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑈 ) )
20 1 2 3 5 7 hlhilplus ⊢ ( 𝜑 → + = ( +g ‘ 𝑈 ) )
21 1 5 8 2 3 hlhilvsca ⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑈 ) )
22 15 a1i ⊢ ( 𝜑 → , = ( ·𝑖 ‘ 𝑈 ) )
23 1 5 2 3 14 hlhil0 ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑈 ) )
24 4 a1i ⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑈 ) )
25 1 5 9 2 4 3 10 hlhilsbase2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐹 ) )
26 1 5 9 2 4 3 11 hlhilsplus2 ⊢ ( 𝜑 → ⨣ = ( +g ‘ 𝐹 ) )
27 1 5 9 2 4 3 12 hlhilsmul2 ⊢ ( 𝜑 → × = ( .r ‘ 𝐹 ) )
28 1 2 4 17 3 hlhilnvl ⊢ ( 𝜑 → 𝐺 = ( *𝑟 ‘ 𝐹 ) )
29 1 5 9 2 4 3 13 hlhils0 ⊢ ( 𝜑 → 𝑄 = ( 0g ‘ 𝐹 ) )
30 1 2 3 hlhillvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
31 1 2 3 4 hlhilsrng ⊢ ( 𝜑 → 𝐹 ∈ *-Ring )
32 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 simp2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
34 simp3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
35 1 5 6 16 2 32 15 33 34 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 , 𝑏 ) = ( ( 𝐽 ‘ 𝑏 ) ‘ 𝑎 ) )
36 1 5 6 9 10 16 32 33 34 hdmapipcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐽 ‘ 𝑏 ) ‘ 𝑎 ) ∈ 𝐵 )
37 35 36 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 , 𝑏 ) ∈ 𝐵 )
38 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
39 simp31 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
40 simp32 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
41 simp33 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → 𝑐 ∈ 𝑉 )
42 simp2 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → 𝑑 ∈ 𝐵 )
43 1 5 6 7 8 9 10 11 12 16 38 39 40 41 42 hdmapln1 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝐽 ‘ 𝑐 ) ‘ ( ( 𝑑 · 𝑎 ) + 𝑏 ) ) = ( ( 𝑑 × ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑎 ) ) ⨣ ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑏 ) ) )
44 1 5 3 dvhlmod ⊢ ( 𝜑 → 𝐿 ∈ LMod )
45 44 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → 𝐿 ∈ LMod )
46 6 9 8 10 lmodvscl ⊢ ( ( 𝐿 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑑 · 𝑎 ) ∈ 𝑉 )
47 45 42 39 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑑 · 𝑎 ) ∈ 𝑉 )
48 6 7 lmodvacl ⊢ ( ( 𝐿 ∈ LMod ∧ ( 𝑑 · 𝑎 ) ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝑑 · 𝑎 ) + 𝑏 ) ∈ 𝑉 )
49 45 47 40 48 syl3anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑑 · 𝑎 ) + 𝑏 ) ∈ 𝑉 )
50 1 5 6 16 2 38 15 49 41 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( ( 𝑑 · 𝑎 ) + 𝑏 ) , 𝑐 ) = ( ( 𝐽 ‘ 𝑐 ) ‘ ( ( 𝑑 · 𝑎 ) + 𝑏 ) ) )
51 1 5 6 16 2 38 15 39 41 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑎 , 𝑐 ) = ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑎 ) )
52 51 oveq2d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑑 × ( 𝑎 , 𝑐 ) ) = ( 𝑑 × ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑎 ) ) )
53 1 5 6 16 2 38 15 40 41 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( 𝑏 , 𝑐 ) = ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑏 ) )
54 52 53 oveq12d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( 𝑑 × ( 𝑎 , 𝑐 ) ) ⨣ ( 𝑏 , 𝑐 ) ) = ( ( 𝑑 × ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑎 ) ) ⨣ ( ( 𝐽 ‘ 𝑐 ) ‘ 𝑏 ) ) )
55 43 50 54 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ) → ( ( ( 𝑑 · 𝑎 ) + 𝑏 ) , 𝑐 ) = ( ( 𝑑 × ( 𝑎 , 𝑐 ) ) ⨣ ( 𝑏 , 𝑐 ) ) )
56 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
58 1 5 6 16 2 56 15 57 57 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 , 𝑎 ) = ( ( 𝐽 ‘ 𝑎 ) ‘ 𝑎 ) )
59 58 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑎 , 𝑎 ) = 𝑄 ↔ ( ( 𝐽 ‘ 𝑎 ) ‘ 𝑎 ) = 𝑄 ) )
60 1 5 6 14 9 13 16 56 57 hdmapip0 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( ( ( 𝐽 ‘ 𝑎 ) ‘ 𝑎 ) = 𝑄 ↔ 𝑎 = 0 ) )
61 59 60 bitrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑎 , 𝑎 ) = 𝑄 ↔ 𝑎 = 0 ) )
62 61 biimp3a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ ( 𝑎 , 𝑎 ) = 𝑄 ) → 𝑎 = 0 )
63 1 5 6 16 17 32 33 34 hdmapg ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐺 ‘ ( ( 𝐽 ‘ 𝑏 ) ‘ 𝑎 ) ) = ( ( 𝐽 ‘ 𝑎 ) ‘ 𝑏 ) )
64 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐺 ‘ ( 𝑎 , 𝑏 ) ) = ( 𝐺 ‘ ( ( 𝐽 ‘ 𝑏 ) ‘ 𝑎 ) ) )
65 1 5 6 16 2 32 15 34 33 hlhilipval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 , 𝑎 ) = ( ( 𝐽 ‘ 𝑎 ) ‘ 𝑏 ) )
66 63 64 65 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐺 ‘ ( 𝑎 , 𝑏 ) ) = ( 𝑏 , 𝑎 ) )
67 19 20 21 22 23 24 25 26 27 28 29 30 31 37 55 62 66 isphld ⊢ ( 𝜑 → 𝑈 ∈ PreHil )