Theorem lclkrslem2

Description: The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace Q is closed under scalar product. (Contributed by NM, 28-Jan-2015)

	Ref	Expression
Hypotheses	lclkrslem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrslem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrslem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrslem1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	lclkrslem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrslem1.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lclkrslem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrslem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lclkrslem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lclkrslem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lclkrslem1.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) }
	lclkrslem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrslem1.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
	lclkrslem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
	lclkrslem2.p	⊢ + = ( +g ‘ 𝐷 )
	lclkrslem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐶 )
Assertion	lclkrslem2	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		lclkrslem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lclkrslem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lclkrslem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lclkrslem1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		lclkrslem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lclkrslem1.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lclkrslem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lclkrslem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
9		lclkrslem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
10		lclkrslem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
11		lclkrslem1.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) }
12		lclkrslem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		lclkrslem1.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
14		lclkrslem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
15		lclkrslem2.p	⊢ + = ( +g ‘ 𝐷 )
16		lclkrslem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐶 )
17		eqid	⊢ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
18	11 17	lcfls1c	⊢ ( 𝐸 ∈ 𝐶 ↔ ( 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) )
19	18	simplbi	⊢ ( 𝐸 ∈ 𝐶 → 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
20	16 19	syl	⊢ ( 𝜑 → 𝐸 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
21	11 17	lcfls1c	⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) )
22	21	simplbi	⊢ ( 𝐺 ∈ 𝐶 → 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
23	14 22	syl	⊢ ( 𝜑 → 𝐺 ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
24	1 2 3 5 6 7 15 17 12 20 23	lclkrlem2	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } )
25		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
26	1 3 12	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
27	11	lcfls1lem	⊢ ( 𝐸 ∈ 𝐶 ↔ ( 𝐸 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) )
28	16 27	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ) )
29	28	simp1d	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
30	11	lcfls1lem	⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) )
31	14 30	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) )
32	31	simp1d	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
33	5 7 15 26 29 32	ldualvaddcl	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
34	25 5 6 26 33	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) )
35	5 6 7 15 26 29 32	lkrin	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) )
36	1 3 25 2	dochss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ⊆ ( Base ‘ 𝑈 ) ∧ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ⊆ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) )
37	12 34 35 36	syl3anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) )
38		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
39		eqid	⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
40	28	simp2d	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) )
41	1 38 2 3 5 6 12 29	lcfl5a	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ) = ( 𝐿 ‘ 𝐸 ) ↔ ( 𝐿 ‘ 𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
42	40 41	mpbid	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
43	31	simp2d	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
44	1 38 2 3 5 6 12 32	lcfl5a	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ↔ ( 𝐿 ‘ 𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
45	43 44	mpbid	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
46	1 38 3 25 2 39 12 42 45	dochdmm1	⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
47		eqid	⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
48	25 5 6 26 29	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) )
49	1 38 3 25 2	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
50	12 48 49	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
51	1 38 2 3 47 5 6 12 50 32	dochkrsm	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
52	1 3 25 4 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐸 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ 𝑆 )
53	12 48 52	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ 𝑆 )
54	25 5 6 26 32	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) )
55	1 3 25 4 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝑆 )
56	12 54 55	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ 𝑆 )
57	1 3 25 4 47 38 39 12 53 56	djhlsmcl	⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) )
58	51 57	mpbid	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
59	46 58	eqtr4d	⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) = ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
60	28	simp3d	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 )
61	31	simp3d	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 )
62	4	lsssssubg	⊢ ( 𝑈 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
63	26 62	syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑈 ) )
64	63 53	sseldd	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
65	63 56	sseldd	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) )
66	63 13	sseldd	⊢ ( 𝜑 → 𝑄 ∈ ( SubGrp ‘ 𝑈 ) )
67	47	lsmlub	⊢ ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ 𝑄 ∈ ( SubGrp ‘ 𝑈 ) ) → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) )
68	64 65 66 67	syl3anc	⊢ ( 𝜑 → ( ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ⊆ 𝑄 ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑄 ) ↔ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 ) )
69	60 61 68	mpbi2and	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐸 ) ) ( LSSum ‘ 𝑈 ) ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 )
70	59 69	eqsstrd	⊢ ( 𝜑 → ( ⊥ ‘ ( ( 𝐿 ‘ 𝐸 ) ∩ ( 𝐿 ‘ 𝐺 ) ) ) ⊆ 𝑄 )
71	37 70	sstrd	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 )
72	11 17	lcfls1c	⊢ ( ( 𝐸 + 𝐺 ) ∈ 𝐶 ↔ ( ( 𝐸 + 𝐺 ) ∈ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } ∧ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐸 + 𝐺 ) ) ) ⊆ 𝑄 ) )
73	24 71 72	sylanbrc	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐶 )