Theorem lcfrlem38

Description: Lemma for lcfr . Combine lcfrlem27 and lcfrlem37 . (Contributed by NM, 11-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem38.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfrlem38.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem38.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfrlem38.p	⊢ + = ( +g ‘ 𝑈 )
	lcfrlem38.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfrlem38.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfrlem38.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem38.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
	lcfrlem38.c	⊢ 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcfrlem38.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfrlem38.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem38.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
	lcfrlem38.gs	⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
	lcfrlem38.xe	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
	lcfrlem38.ye	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
	lcfrlem38.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcfrlem38.x	⊢ ( 𝜑 → 𝑋 ≠ 0 )
	lcfrlem38.y	⊢ ( 𝜑 → 𝑌 ≠ 0 )
	lcfrlem38.sp	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	lcfrlem38.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
	lcfrlem38.b	⊢ 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
	lcfrlem38.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
	lcfrlem38.n	⊢ ( 𝜑 → 𝐼 ≠ 0 )
	lcfrlem38.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfrlem38.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcfrlem38.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfrlem38.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcfrlem38.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
Assertion	lcfrlem38	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem38.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfrlem38.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfrlem38.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfrlem38.p	⊢ + = ( +g ‘ 𝑈 )
5		lcfrlem38.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcfrlem38.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcfrlem38.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfrlem38.q	⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
9		lcfrlem38.c	⊢ 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
10		lcfrlem38.e	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
11		lcfrlem38.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		lcfrlem38.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
13		lcfrlem38.gs	⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
14		lcfrlem38.xe	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
15		lcfrlem38.ye	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
16		lcfrlem38.z	⊢ 0 = ( 0g ‘ 𝑈 )
17		lcfrlem38.x	⊢ ( 𝜑 → 𝑋 ≠ 0 )
18		lcfrlem38.y	⊢ ( 𝜑 → 𝑌 ≠ 0 )
19		lcfrlem38.sp	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
20		lcfrlem38.ne	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
21		lcfrlem38.b	⊢ 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
22		lcfrlem38.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
23		lcfrlem38.n	⊢ ( 𝜑 → 𝐼 ≠ 0 )
24		lcfrlem38.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
25		lcfrlem38.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
26		lcfrlem38.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
27		lcfrlem38.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
28		lcfrlem38.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
29		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
30	11	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
31	1 2 3 24 6 7 8 10 11 12 14	lcfrlem4	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
32		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
33	31 17 32	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
35	1 2 3 24 6 7 8 10 11 12 15	lcfrlem4	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
36		eldifsn	⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ) )
37	35 18 36	sylanbrc	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
39	20	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
40		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
41	22	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝐼 ∈ 𝐵 )
42		simpr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) )
43	23	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝐼 ≠ 0 )
44	12 8	eleqtrdi	⊢ ( 𝜑 → 𝐺 ∈ ( LSubSp ‘ 𝐷 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝐷 ) )
46	13 9	sseqtrdi	⊢ ( 𝜑 → 𝐺 ⊆ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
47	46	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝐺 ⊆ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
48	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝑋 ∈ 𝐸 )
49	15	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → 𝑌 ∈ 𝐸 )
50	1 2 3 24 4 16 19 29 30 34 38 39 21 25 26 40 27 28 41 6 7 42 43 45 47 10 48 49	lcfrlem27	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) = ( 0g ‘ 𝑆 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐸 )
51	11	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
52	33	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
53	37	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
54	20	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
55	22	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝐼 ∈ 𝐵 )
56		simpr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) )
57		eqid	⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
58		eqid	⊢ ( -g ‘ 𝐷 ) = ( -g ‘ 𝐷 )
59		eqid	⊢ ( ( 𝐽 ‘ 𝑋 ) ( -g ‘ 𝐷 ) ( ( ( ( invr ‘ 𝑆 ) ‘ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ) ( .r ‘ 𝑆 ) ( ( 𝐽 ‘ 𝑋 ) ‘ 𝐼 ) ) ( ·𝑠 ‘ 𝐷 ) ( 𝐽 ‘ 𝑌 ) ) ) = ( ( 𝐽 ‘ 𝑋 ) ( -g ‘ 𝐷 ) ( ( ( ( invr ‘ 𝑆 ) ‘ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ) ( .r ‘ 𝑆 ) ( ( 𝐽 ‘ 𝑋 ) ‘ 𝐼 ) ) ( ·𝑠 ‘ 𝐷 ) ( 𝐽 ‘ 𝑌 ) ) )
60	44	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝐷 ) )
61	46	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝐺 ⊆ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
62	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝑋 ∈ 𝐸 )
63	15	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → 𝑌 ∈ 𝐸 )
64	1 2 3 24 4 16 19 29 51 52 53 54 21 25 26 40 27 28 55 6 7 56 57 58 59 60 61 10 62 63	lcfrlem37	⊢ ( ( 𝜑 ∧ ( ( 𝐽 ‘ 𝑌 ) ‘ 𝐼 ) ≠ ( 0g ‘ 𝑆 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐸 )
65	50 64	pm2.61dane	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )