Theorem lcfrlem4

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

	Ref	Expression
Hypotheses	lcfrlem4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrlem4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem4.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfrlem4.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrlem4.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem4.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
	lcfrlem4.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfrlem4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
	lcfrlem4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
Assertion	lcfrlem4	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrlem4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrlem4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrlem4.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfrlem4.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
6		lcfrlem4.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lcfrlem4.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
8		lcfrlem4.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
9		lcfrlem4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcfrlem4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
11		lcfrlem4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
12	9	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
14	1 3 9	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑈 ∈ LMod )
16		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
17	16 7	lssel	⊢ ( ( 𝐺 ∈ 𝑄 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
18	10 17	sylan	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
19	13 6 16 14	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( LFnl ‘ 𝑈 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( Base ‘ 𝐷 ) = ( LFnl ‘ 𝑈 ) )
21	18 20	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( LFnl ‘ 𝑈 ) )
22	4 13 5 15 21	lkrssv	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 )
23	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
24	12 22 23	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
26		iunss	⊢ ( ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 ↔ ∀ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
27	25 26	sylibr	⊢ ( 𝜑 → ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
28	11 8	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
29	27 28	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )