Metamath Proof Explorer

Theorem hlhilhillem

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 ⊢ 𝐸 = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( ( 𝐽 ‘ 𝑦 ) ‘ 𝑥 ) )
hlhilphllem.o ⊢ 𝑂 = ( ocv ‘ 𝑈 )
hlhilphllem.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑈 )
Assertion hlhilhillem ( 𝜑 → 𝑈 ∈ Hil )

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 hlhilphllem.o ⊢ 𝑂 = ( ocv ‘ 𝑈 )
20 hlhilphllem.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑈 )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hlhilphllem ⊢ ( 𝜑 → 𝑈 ∈ PreHil )
22 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
24 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
25 1 24 2 20 3 hlhillcs ⊢ ( 𝜑 → 𝐶 = ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 25 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
27 26 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
28 1 5 24 6 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 ⊆ 𝑉 )
29 3 28 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 ⊆ 𝑉 )
30 27 29 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ⊆ 𝑉 )
31 1 5 2 22 6 23 19 30 hlhilocv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑂 ‘ 𝑥 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) )
32 31 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ( LSSum ‘ 𝐿 ) ( 𝑂 ‘ 𝑥 ) ) = ( 𝑥 ( LSSum ‘ 𝐿 ) ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
33 eqid ⊢ ( LSSum ‘ 𝐿 ) = ( LSSum ‘ 𝐿 )
34 1 5 2 3 33 hlhillsm ⊢ ( 𝜑 → ( LSSum ‘ 𝐿 ) = ( LSSum ‘ 𝑈 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( LSSum ‘ 𝐿 ) = ( LSSum ‘ 𝑈 ) )
36 35 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ( LSSum ‘ 𝐿 ) ( 𝑂 ‘ 𝑥 ) ) = ( 𝑥 ( LSSum ‘ 𝑈 ) ( 𝑂 ‘ 𝑥 ) ) )
37 eqid ⊢ ( LSubSp ‘ 𝐿 ) = ( LSubSp ‘ 𝐿 )
38 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
39 1 5 24 37 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 ∈ ( LSubSp ‘ 𝐿 ) )
40 3 39 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 ∈ ( LSubSp ‘ 𝐿 ) )
41 1 24 5 6 23 38 29 dochoccl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
42 41 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
43 42 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) → ( 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) ) )
44 43 pm2.43d ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 ) )
45 44 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑥 )
46 1 23 5 6 37 33 38 40 45 dochexmid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ( LSSum ‘ 𝐿 ) ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑉 )
47 27 46 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ( LSSum ‘ 𝐿 ) ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = 𝑉 )
48 32 36 47 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ( LSSum ‘ 𝑈 ) ( 𝑂 ‘ 𝑥 ) ) = 𝑉 )
49 1 2 3 5 6 hlhilbase ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑈 ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑉 = ( Base ‘ 𝑈 ) )
51 48 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ( LSSum ‘ 𝑈 ) ( 𝑂 ‘ 𝑥 ) ) = ( Base ‘ 𝑈 ) )
52 51 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ( 𝑥 ( LSSum ‘ 𝑈 ) ( 𝑂 ‘ 𝑥 ) ) = ( Base ‘ 𝑈 ) )
53 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
54 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
55 53 54 19 20 ishil2 ⊢ ( 𝑈 ∈ Hil ↔ ( 𝑈 ∈ PreHil ∧ ∀ 𝑥 ∈ 𝐶 ( 𝑥 ( LSSum ‘ 𝑈 ) ( 𝑂 ‘ 𝑥 ) ) = ( Base ‘ 𝑈 ) ) )
56 21 52 55 sylanbrc ⊢ ( 𝜑 → 𝑈 ∈ Hil )