Theorem lclkrlem1

Description: The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014)

	Ref	Expression
Hypotheses	lclkrlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrlem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrlem1.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lclkrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lclkrlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lclkrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lclkrlem1.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lclkrlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	lclkrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
Assertion	lclkrlem1	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lclkrlem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lclkrlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lclkrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5		lclkrlem1.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
6		lclkrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lclkrlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
8		lclkrlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
9		lclkrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
10		lclkrlem1.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
11		lclkrlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		lclkrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13		lclkrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐶 )
14	1 3 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	10	lcfl1lem	⊢ ( 𝐺 ∈ 𝐶 ↔ ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
16	13 15	sylib	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
17	16	simpld	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
18	4 7 8 6 9 14 12 17	ldualvscl	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐹 )
19		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20	1 3 2 19 11	dochoc1	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
22		fvoveq1	⊢ ( 𝑋 = ( 0g ‘ 𝑅 ) → ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) = ( 𝐿 ‘ ( ( 0g ‘ 𝑅 ) · 𝐺 ) ) )
23	6 14	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
24		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
25	4 6 24 14 17	ldualelvbase	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
26		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
27		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
28		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
29	24 26 9 27 28	lmod0vs	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = ( 0g ‘ 𝐷 ) )
30	23 25 29	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = ( 0g ‘ 𝐷 ) )
31		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
32	7 31 6 26 27 14	ldual0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ 𝑅 ) )
33	32	oveq1d	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = ( ( 0g ‘ 𝑅 ) · 𝐺 ) )
34	19 7 31 6 28 14	ldual0v	⊢ ( 𝜑 → ( 0g ‘ 𝐷 ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) )
35	30 33 34	3eqtr3d	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) · 𝐺 ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) )
36	35	fveq2d	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 0g ‘ 𝑅 ) · 𝐺 ) ) = ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) )
37		eqid	⊢ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } )
38	7 31 19 4	lfl0f	⊢ ( 𝑈 ∈ LMod → ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ∈ 𝐹 )
39	7 31 19 4 5	lkr0f	⊢ ( ( 𝑈 ∈ LMod ∧ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ∈ 𝐹 ) → ( ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) = ( Base ‘ 𝑈 ) ↔ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) )
40	14 38 39	syl2anc2	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) = ( Base ‘ 𝑈 ) ↔ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) )
41	37 40	mpbiri	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( Base ‘ 𝑈 ) × { ( 0g ‘ 𝑅 ) } ) ) = ( Base ‘ 𝑈 ) )
42	36 41	eqtrd	⊢ ( 𝜑 → ( 𝐿 ‘ ( ( 0g ‘ 𝑅 ) · 𝐺 ) ) = ( Base ‘ 𝑈 ) )
43	22 42	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) = ( Base ‘ 𝑈 ) )
44	43	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) = ( ⊥ ‘ ( Base ‘ 𝑈 ) ) )
45	44	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( Base ‘ 𝑈 ) ) ) )
46	21 45 43	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) )
47	16	simprd	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
49	1 3 11	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑈 ∈ LVec )
51	17	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝐺 ∈ 𝐹 )
52	12	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
53		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → 𝑋 ≠ ( 0g ‘ 𝑅 ) )
54	7 8 31 4 5 6 9 50 51 52 53	ldualkrsc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) = ( 𝐿 ‘ 𝐺 ) )
55	54	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
56	55	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
57	48 56 54	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑅 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) )
58	46 57	pm2.61dane	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) )
59	10	lcfl1lem	⊢ ( ( 𝑋 · 𝐺 ) ∈ 𝐶 ↔ ( ( 𝑋 · 𝐺 ) ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) ) = ( 𝐿 ‘ ( 𝑋 · 𝐺 ) ) ) )
60	18 58 59	sylanbrc	⊢ ( 𝜑 → ( 𝑋 · 𝐺 ) ∈ 𝐶 )