Metamath Proof Explorer

Theorem lcfrlem4

Description: Lemma for lcfr . (Contributed by NM, 10-Mar-2015)

Ref Expression
Hypotheses lcfrlem4.h ⊢ H = LHyp ⁡ K
lcfrlem4.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
lcfrlem4.u ⊢ U = DVecH ⁡ K ⁡ W
lcfrlem4.v ⊢ V = Base U
lcfrlem4.l ⊢ L = LKer ⁡ U
lcfrlem4.d ⊢ D = LDual ⁡ U
lcfrlem4.q ⊢ Q = LSubSp ⁡ D
lcfrlem4.e ⊢ E = ⋃ g ∈ G ⊥ ˙ ⁡ L ⁡ g
lcfrlem4.k ⊢ φ → K ∈ HL ∧ W ∈ H
lcfrlem4.g ⊢ φ → G ∈ Q
lcfrlem4.x ⊢ φ → X ∈ E
Assertion lcfrlem4 ⊢ φ → X ∈ V

Proof

Step Hyp Ref Expression
1 lcfrlem4.h ⊢ H = LHyp ⁡ K
2 lcfrlem4.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 lcfrlem4.u ⊢ U = DVecH ⁡ K ⁡ W
4 lcfrlem4.v ⊢ V = Base U
5 lcfrlem4.l ⊢ L = LKer ⁡ U
6 lcfrlem4.d ⊢ D = LDual ⁡ U
7 lcfrlem4.q ⊢ Q = LSubSp ⁡ D
8 lcfrlem4.e ⊢ E = ⋃ g ∈ G ⊥ ˙ ⁡ L ⁡ g
9 lcfrlem4.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 lcfrlem4.g ⊢ φ → G ∈ Q
11 lcfrlem4.x ⊢ φ → X ∈ E
12 9 adantr ⊢ φ ∧ g ∈ G → K ∈ HL ∧ W ∈ H
13 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
14 1 3 9 dvhlmod ⊢ φ → U ∈ LMod
15 14 adantr ⊢ φ ∧ g ∈ G → U ∈ LMod
16 eqid ⊢ Base D = Base D
17 16 7 lssel ⊢ G ∈ Q ∧ g ∈ G → g ∈ Base D
18 10 17 sylan ⊢ φ ∧ g ∈ G → g ∈ Base D
19 13 6 16 14 ldualvbase ⊢ φ → Base D = LFnl ⁡ U
20 19 adantr ⊢ φ ∧ g ∈ G → Base D = LFnl ⁡ U
21 18 20 eleqtrd ⊢ φ ∧ g ∈ G → g ∈ LFnl ⁡ U
22 4 13 5 15 21 lkrssv ⊢ φ ∧ g ∈ G → L ⁡ g ⊆ V
23 1 3 4 2 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ L ⁡ g ⊆ V → ⊥ ˙ ⁡ L ⁡ g ⊆ V
24 12 22 23 syl2anc ⊢ φ ∧ g ∈ G → ⊥ ˙ ⁡ L ⁡ g ⊆ V
25 24 ralrimiva ⊢ φ → ∀ g ∈ G ⊥ ˙ ⁡ L ⁡ g ⊆ V
26 iunss ⊢ ⋃ g ∈ G ⊥ ˙ ⁡ L ⁡ g ⊆ V ↔ ∀ g ∈ G ⊥ ˙ ⁡ L ⁡ g ⊆ V
27 25 26 sylibr ⊢ φ → ⋃ g ∈ G ⊥ ˙ ⁡ L ⁡ g ⊆ V
28 11 8 eleqtrdi ⊢ φ → X ∈ ⋃ g ∈ G ⊥ ˙ ⁡ L ⁡ g
29 27 28 sseldd ⊢ φ → X ∈ V