Metamath Proof Explorer

Theorem hlhilhillem

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

Ref Expression
Hypotheses hlhilphl.h ⊢ H = LHyp ⁡ K
hlhilphllem.u ⊢ U = HLHil ⁡ K ⁡ W
hlhilphl.k ⊢ φ → K ∈ HL ∧ W ∈ H
hlhilphllem.f ⊢ F = Scalar ⁡ U
hlhilphllem.l ⊢ L = DVecH ⁡ K ⁡ W
hlhilphllem.v ⊢ V = Base L
hlhilphllem.a ⊢ + ˙ = + L
hlhilphllem.s ⊢ · ˙ = ⋅ L
hlhilphllem.r ⊢ R = Scalar ⁡ L
hlhilphllem.b ⊢ B = Base R
hlhilphllem.p ⊢ ⨣ ˙ = + R
hlhilphllem.t ⊢ × ˙ = ⋅ R
hlhilphllem.q ⊢ Q = 0 R
hlhilphllem.z ⊢ 0 ˙ = 0 L
hlhilphllem.i ⊢ , ˙ = ⋅ 𝑖 ⁡ U
hlhilphllem.j ⊢ J = HDMap ⁡ K ⁡ W
hlhilphllem.g ⊢ G = HGMap ⁡ K ⁡ W
hlhilphllem.e ⊢ E = x ∈ V , y ∈ V ⟼ J ⁡ y ⁡ x
hlhilphllem.o ⊢ O = ocv ⁡ U
hlhilphllem.c ⊢ C = ClSubSp ⁡ U
Assertion hlhilhillem ⊢ φ → U ∈ Hil

Proof

Step Hyp Ref Expression
1 hlhilphl.h ⊢ H = LHyp ⁡ K
2 hlhilphllem.u ⊢ U = HLHil ⁡ K ⁡ W
3 hlhilphl.k ⊢ φ → K ∈ HL ∧ W ∈ H
4 hlhilphllem.f ⊢ F = Scalar ⁡ U
5 hlhilphllem.l ⊢ L = DVecH ⁡ K ⁡ W
6 hlhilphllem.v ⊢ V = Base L
7 hlhilphllem.a ⊢ + ˙ = + L
8 hlhilphllem.s ⊢ · ˙ = ⋅ L
9 hlhilphllem.r ⊢ R = Scalar ⁡ L
10 hlhilphllem.b ⊢ B = Base R
11 hlhilphllem.p ⊢ ⨣ ˙ = + R
12 hlhilphllem.t ⊢ × ˙ = ⋅ R
13 hlhilphllem.q ⊢ Q = 0 R
14 hlhilphllem.z ⊢ 0 ˙ = 0 L
15 hlhilphllem.i ⊢ , ˙ = ⋅ 𝑖 ⁡ U
16 hlhilphllem.j ⊢ J = HDMap ⁡ K ⁡ W
17 hlhilphllem.g ⊢ G = HGMap ⁡ K ⁡ W
18 hlhilphllem.e ⊢ E = x ∈ V , y ∈ V ⟼ J ⁡ y ⁡ x
19 hlhilphllem.o ⊢ O = ocv ⁡ U
20 hlhilphllem.c ⊢ C = ClSubSp ⁡ U
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hlhilphllem ⊢ φ → U ∈ PreHil
22 3 adantr ⊢ φ ∧ x ∈ C → K ∈ HL ∧ W ∈ H
23 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
24 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
25 1 24 2 20 3 hlhillcs ⊢ φ → C = ran ⁡ DIsoH ⁡ K ⁡ W
26 25 eleq2d ⊢ φ → x ∈ C ↔ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
27 26 biimpa ⊢ φ ∧ x ∈ C → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
28 1 5 24 6 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ⊆ V
29 3 28 sylan ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ⊆ V
30 27 29 syldan ⊢ φ ∧ x ∈ C → x ⊆ V
31 1 5 2 22 6 23 19 30 hlhilocv ⊢ φ ∧ x ∈ C → O ⁡ x = ocH ⁡ K ⁡ W ⁡ x
32 31 oveq2d ⊢ φ ∧ x ∈ C → x LSSum ⁡ L O ⁡ x = x LSSum ⁡ L ocH ⁡ K ⁡ W ⁡ x
33 eqid ⊢ LSSum ⁡ L = LSSum ⁡ L
34 1 5 2 3 33 hlhillsm ⊢ φ → LSSum ⁡ L = LSSum ⁡ U
35 34 adantr ⊢ φ ∧ x ∈ C → LSSum ⁡ L = LSSum ⁡ U
36 35 oveqd ⊢ φ ∧ x ∈ C → x LSSum ⁡ L O ⁡ x = x LSSum ⁡ U O ⁡ x
37 eqid ⊢ LSubSp ⁡ L = LSubSp ⁡ L
38 3 adantr ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → K ∈ HL ∧ W ∈ H
39 1 5 24 37 dihrnlss ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ∈ LSubSp ⁡ L
40 3 39 sylan ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ∈ LSubSp ⁡ L
41 1 24 5 6 23 38 29 dochoccl ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W ↔ ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ x = x
42 41 biimpd ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ x = x
43 42 ex ⊢ φ → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ x = x
44 43 pm2.43d ⊢ φ → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ x = x
45 44 imp ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ x = x
46 1 23 5 6 37 33 38 40 45 dochexmid ⊢ φ ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → x LSSum ⁡ L ocH ⁡ K ⁡ W ⁡ x = V
47 27 46 syldan ⊢ φ ∧ x ∈ C → x LSSum ⁡ L ocH ⁡ K ⁡ W ⁡ x = V
48 32 36 47 3eqtr3d ⊢ φ ∧ x ∈ C → x LSSum ⁡ U O ⁡ x = V
49 1 2 3 5 6 hlhilbase ⊢ φ → V = Base U
50 49 adantr ⊢ φ ∧ x ∈ C → V = Base U
51 48 50 eqtrd ⊢ φ ∧ x ∈ C → x LSSum ⁡ U O ⁡ x = Base U
52 51 ralrimiva ⊢ φ → ∀ x ∈ C x LSSum ⁡ U O ⁡ x = Base U
53 eqid ⊢ Base U = Base U
54 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
55 53 54 19 20 ishil2 ⊢ U ∈ Hil ↔ U ∈ PreHil ∧ ∀ x ∈ C x LSSum ⁡ U O ⁡ x = Base U
56 21 52 55 sylanbrc ⊢ φ → U ∈ Hil