Theorem lclkrlem2m

Description: Lemma for lclkr . Construct a vector B that makes the sum of functionals zero. Combine with B e. V to shorten overall proof. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lclkrlem2m.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lclkrlem2m.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lclkrlem2m.q	⊢ × = ( .r ‘ 𝑆 )
	lclkrlem2m.z	⊢ 0 = ( 0g ‘ 𝑆 )
	lclkrlem2m.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
	lclkrlem2m.m	⊢ − = ( -g ‘ 𝑈 )
	lclkrlem2m.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrlem2m.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrlem2m.p	⊢ + = ( +g ‘ 𝐷 )
	lclkrlem2m.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lclkrlem2m.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lclkrlem2m.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
	lclkrlem2m.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lclkrlem2m.w	⊢ ( 𝜑 → 𝑈 ∈ LVec )
	lclkrlem2m.b	⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
	lclkrlem2m.n	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
Assertion	lclkrlem2m	⊢ ( 𝜑 → ( 𝐵 ∈ 𝑉 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
2		lclkrlem2m.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
3		lclkrlem2m.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4		lclkrlem2m.q	⊢ × = ( .r ‘ 𝑆 )
5		lclkrlem2m.z	⊢ 0 = ( 0g ‘ 𝑆 )
6		lclkrlem2m.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
7		lclkrlem2m.m	⊢ − = ( -g ‘ 𝑈 )
8		lclkrlem2m.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9		lclkrlem2m.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
10		lclkrlem2m.p	⊢ + = ( +g ‘ 𝐷 )
11		lclkrlem2m.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12		lclkrlem2m.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
13		lclkrlem2m.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
14		lclkrlem2m.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15		lclkrlem2m.w	⊢ ( 𝜑 → 𝑈 ∈ LVec )
16		lclkrlem2m.b	⊢ 𝐵 = ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) )
17		lclkrlem2m.n	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 )
18		lveclmod	⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19	15 18	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20		lmodgrp	⊢ ( 𝑈 ∈ LMod → 𝑈 ∈ Grp )
21	19 20	syl	⊢ ( 𝜑 → 𝑈 ∈ Grp )
22	3	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
23	19 22	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
24	8 9 10 19 13 14	ldualvaddcl	⊢ ( 𝜑 → ( 𝐸 + 𝐺 ) ∈ 𝐹 )
25		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
26	3 25 1 8	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
27	15 24 11 26	syl3anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
28	3	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
29	15 28	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
30	3 25 1 8	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
31	15 24 12 30	syl3anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
32	25 5 6	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
33	29 31 17 32	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) )
34	25 4	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
35	23 27 33 34	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) )
36	1 3 2 25	lmodvscl	⊢ ( ( 𝑈 ∈ LMod ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
37	19 35 12 36	syl3anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 )
38	1 7	grpsubcl	⊢ ( ( 𝑈 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 ) → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ 𝑉 )
39	21 11 37 38	syl3anc	⊢ ( 𝜑 → ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ∈ 𝑉 )
40	16 39	eqeltrid	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
41	16	fveq2i	⊢ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) )
42		eqid	⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
43	3 42 1 7 8	lflsub	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ ( 𝑋 ∈ 𝑉 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ∈ 𝑉 ) ) → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) )
44	19 24 11 37 43	syl112anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) )
45	3 25 4 1 2 8	lflmul	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐸 + 𝐺 ) ∈ 𝐹 ∧ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 ∈ 𝑉 ) ) → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) )
46	19 24 35 12 45	syl112anc	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) )
47	25 4	ringass	⊢ ( ( 𝑆 ∈ Ring ∧ ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) )
48	23 27 33 31 47	syl13anc	⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) )
49		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
50	25 5 4 49 6	drnginvrl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ≠ 0 ) → ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( 1r ‘ 𝑆 ) )
51	29 31 17 50	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( 1r ‘ 𝑆 ) )
52	51	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) )
53	48 52	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) × ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) )
54	25 4 49	ringridm	⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
55	23 27 54	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 1r ‘ 𝑆 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
56	46 53 55	3eqtrd	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) = ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) )
57	56	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) )
58		ringgrp	⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
59	23 58	syl	⊢ ( 𝜑 → 𝑆 ∈ Grp )
60	25 5 42	grpsubid	⊢ ( ( 𝑆 ∈ Grp ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) = 0 )
61	59 27 60	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) ) = 0 )
62	44 57 61	3eqtrd	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ ( 𝑋 − ( ( ( ( 𝐸 + 𝐺 ) ‘ 𝑋 ) × ( 𝐼 ‘ ( ( 𝐸 + 𝐺 ) ‘ 𝑌 ) ) ) · 𝑌 ) ) ) = 0 )
63	41 62	eqtrid	⊢ ( 𝜑 → ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 )
64	40 63	jca	⊢ ( 𝜑 → ( 𝐵 ∈ 𝑉 ∧ ( ( 𝐸 + 𝐺 ) ‘ 𝐵 ) = 0 ) )