Theorem lcfrlem1

Description: Lemma for lcfr . Note that X is z in Mario's notes. (Contributed by NM, 27-Feb-2015)

	Ref	Expression
Hypotheses	lcfrlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfrlem1.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfrlem1.q	⊢ × = ( .r ‘ 𝑆 )
	lcfrlem1.z	⊢ 0 = ( 0g ‘ 𝑆 )
	lcfrlem1.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
	lcfrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcfrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	lcfrlem1.m	⊢ − = ( -g ‘ 𝐷 )
	lcfrlem1.u	⊢ ( 𝜑 → 𝑈 ∈ LVec )
	lcfrlem1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
	lcfrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcfrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lcfrlem1.n	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
	lcfrlem1.h	⊢ 𝐻 = ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) )
Assertion	lcfrlem1	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
2		lcfrlem1.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
3		lcfrlem1.q	⊢ × = ( .r ‘ 𝑆 )
4		lcfrlem1.z	⊢ 0 = ( 0g ‘ 𝑆 )
5		lcfrlem1.i	⊢ 𝐼 = ( invr ‘ 𝑆 )
6		lcfrlem1.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcfrlem1.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lcfrlem1.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
9		lcfrlem1.m	⊢ − = ( -g ‘ 𝐷 )
10		lcfrlem1.u	⊢ ( 𝜑 → 𝑈 ∈ LVec )
11		lcfrlem1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐹 )
12		lcfrlem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
13		lcfrlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14		lcfrlem1.n	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
15		lcfrlem1.h	⊢ 𝐻 = ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) )
16	15	fveq1i	⊢ ( 𝐻 ‘ 𝑋 ) = ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 )
17		eqid	⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
18		lveclmod	⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
19	10 18	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
20		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
21	2	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑆 ∈ DivRing )
22	10 21	syl	⊢ ( 𝜑 → 𝑆 ∈ DivRing )
23	2 20 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
24	10 12 13 23	syl3anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
25	20 4 5	drnginvrcl	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
26	22 24 14 25	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
27	2 20 1 6	lflcl	⊢ ( ( 𝑈 ∈ LVec ∧ 𝐸 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
28	10 11 13 27	syl3anc	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) )
29	2 20 3	lmodmcl	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
30	19 26 28 29	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) )
31	6 2 20 7 8 19 30 12	ldualvscl	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ∈ 𝐹 )
32	1 2 17 6 7 9 19 11 31 13	ldualvsubval	⊢ ( 𝜑 → ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 ) = ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) ) )
33	6 1 2 20 3 7 8 10 30 12 13	ldualvsval	⊢ ( 𝜑 → ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
34		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
35	20 4 3 34 5	drnginvrr	⊢ ( ( 𝑆 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑆 ) )
36	22 24 14 35	syl3anc	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑆 ) )
37	36	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) )
38	2	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Ring )
39	19 38	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
40	20 3	ringass	⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
41	39 24 26 28 40	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝑋 ) × ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) ) × ( 𝐸 ‘ 𝑋 ) ) = ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) )
42	20 3 34	ringlidm	⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) = ( 𝐸 ‘ 𝑋 ) )
43	39 28 42	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) × ( 𝐸 ‘ 𝑋 ) ) = ( 𝐸 ‘ 𝑋 ) )
44	37 41 43	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) × ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) ) = ( 𝐸 ‘ 𝑋 ) )
45	33 44	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) = ( 𝐸 ‘ 𝑋 ) )
46	45	oveq2d	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ‘ 𝑋 ) ) = ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) )
47	2	lmodfgrp	⊢ ( 𝑈 ∈ LMod → 𝑆 ∈ Grp )
48	19 47	syl	⊢ ( 𝜑 → 𝑆 ∈ Grp )
49	20 4 17	grpsubid	⊢ ( ( 𝑆 ∈ Grp ∧ ( 𝐸 ‘ 𝑋 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) = 0 )
50	48 28 49	syl2anc	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) ( -g ‘ 𝑆 ) ( 𝐸 ‘ 𝑋 ) ) = 0 )
51	32 46 50	3eqtrd	⊢ ( 𝜑 → ( ( 𝐸 − ( ( ( 𝐼 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐸 ‘ 𝑋 ) ) · 𝐺 ) ) ‘ 𝑋 ) = 0 )
52	16 51	eqtrid	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = 0 )