This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )