Theorem lduallmodlem

Description: Lemma for lduallmod . (Contributed by NM, 22-Oct-2014)

	Ref	Expression
Hypotheses	lduallmod.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	lduallmod.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lduallmod.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lduallmod.p	⊢ + = ∘f ( +g ‘ 𝑊 )
	lduallmod.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lduallmod.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	lduallmod.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	lduallmod.t	⊢ × = ( .r ‘ 𝑅 )
	lduallmod.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	lduallmod.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
Assertion	lduallmodlem	⊢ ( 𝜑 → 𝐷 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		lduallmod.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
2		lduallmod.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
3		lduallmod.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lduallmod.p	⊢ + = ∘f ( +g ‘ 𝑊 )
5		lduallmod.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6		lduallmod.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
7		lduallmod.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
8		lduallmod.t	⊢ × = ( .r ‘ 𝑅 )
9		lduallmod.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
10		lduallmod.s	⊢ · = ( ·𝑠 ‘ 𝐷 )
11		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12	5 1 11 2	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
13	12	eqcomd	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐷 ) )
14		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) )
15		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
16	6 9 1 15 2	ldualsca	⊢ ( 𝜑 → ( Scalar ‘ 𝐷 ) = 𝑂 )
17	16	eqcomd	⊢ ( 𝜑 → 𝑂 = ( Scalar ‘ 𝐷 ) )
18	10	a1i	⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝐷 ) )
19	9 7	opprbas	⊢ 𝐾 = ( Base ‘ 𝑂 )
20	19	a1i	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑂 ) )
21		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
22	9 21	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
23	22	a1i	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 ) )
24	16	fveq2d	⊢ ( 𝜑 → ( .r ‘ ( Scalar ‘ 𝐷 ) ) = ( .r ‘ 𝑂 ) )
25		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26	9 25	oppr1	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑂 )
27	26	a1i	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑂 ) )
28	6	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
29	9	opprring	⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
30	2 28 29	3syl	⊢ ( 𝜑 → 𝑂 ∈ Ring )
31	1 2	ldualgrp	⊢ ( 𝜑 → 𝐷 ∈ Grp )
32	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ) → 𝑊 ∈ LMod )
33		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ) → 𝑥 ∈ 𝐾 )
34		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ∈ 𝐹 )
35	5 6 7 1 10 32 33 34	ldualvscl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
36		eqid	⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
37	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑊 ∈ LMod )
38		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐾 )
39		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐹 )
40		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑧 ∈ 𝐹 )
41	5 6 7 1 36 10 37 38 39 40	ldualvsdi1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑥 · ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝐷 ) ( 𝑥 · 𝑧 ) ) )
42	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑊 ∈ LMod )
43		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐾 )
44		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐾 )
45		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑧 ∈ 𝐹 )
46	5 6 21 7 1 36 10 42 43 44 45	ldualvsdi2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝐷 ) ( 𝑦 · 𝑧 ) ) )
47		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝐷 ) ) = ( .r ‘ ( Scalar ‘ 𝐷 ) )
48	5 6 7 1 15 47 10 42 43 44 45	ldualvsass2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( .r ‘ ( Scalar ‘ 𝐷 ) ) 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
49	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → 𝑊 ∈ LMod )
50	7 25	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
51	2 28 50	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
53		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
54	5 3 6 7 8 1 10 49 52 53	ldualvs	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 1r ‘ 𝑅 ) · 𝑥 ) = ( 𝑥 ∘f × ( 𝑉 × { ( 1r ‘ 𝑅 ) } ) ) )
55	3 6 5 7 8 25 49 53	lfl1sc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∘f × ( 𝑉 × { ( 1r ‘ 𝑅 ) } ) ) = 𝑥 )
56	54 55	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 1r ‘ 𝑅 ) · 𝑥 ) = 𝑥 )
57	13 14 17 18 20 23 24 27 30 31 35 41 46 48 56	islmodd	⊢ ( 𝜑 → 𝐷 ∈ LMod )