Metamath Proof Explorer

Theorem ldualgrplem

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

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

Proof

Step Hyp Ref Expression
1 ldualgrp.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
2 ldualgrp.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
3 ldualgrp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ldualgrp.p ⊢ + = ∘f ( +g ‘ 𝑊 )
5 ldualgrp.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 ldualgrp.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
7 ldualgrp.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
8 ldualgrp.t ⊢ × = ( .r ‘ 𝑅 )
9 ldualgrp.o ⊢ 𝑂 = ( oppr ‘ 𝑅 )
10 ldualgrp.s ⊢ · = ( ·𝑠 ‘ 𝐷 )
11 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12 5 1 11 2 ldualvbase ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
13 12 eqcomd ⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐷 ) )
14 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 ) )
15 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
16 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → 𝑊 ∈ LMod )
17 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
18 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ∈ 𝐹 )
19 5 1 15 16 17 18 ldualvaddcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ∈ 𝐹 )
20 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
21 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑊 ∈ LMod )
22 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑦 ∈ 𝐹 )
23 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑧 ∈ 𝐹 )
24 5 6 20 1 15 21 22 23 ldualvadd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
25 24 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑥 ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) )
26 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → 𝑥 ∈ 𝐹 )
27 5 1 15 21 22 23 ldualvaddcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ∈ 𝐹 )
28 5 6 20 1 15 21 26 27 ldualvadd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐷 ) ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ) )
29 5 1 15 21 26 22 ldualvaddcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ∈ 𝐹 )
30 5 6 20 1 15 21 29 23 ldualvadd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ( +g ‘ 𝐷 ) 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
31 5 6 20 1 15 21 26 22 ldualvadd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
32 31 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
33 6 20 5 21 26 22 23 lfladdass ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) )
34 30 32 33 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ( +g ‘ 𝐷 ) 𝑧 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) )
35 25 28 34 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝐷 ) 𝑦 ) ( +g ‘ 𝐷 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐷 ) ( 𝑦 ( +g ‘ 𝐷 ) 𝑧 ) ) )
36 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
37 6 36 3 5 lfl0f ⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ∈ 𝐹 )
38 2 37 syl ⊢ ( 𝜑 → ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ∈ 𝐹 )
39 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → 𝑊 ∈ LMod )
40 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ∈ 𝐹 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
42 5 6 20 1 15 39 40 41 ldualvadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ( +g ‘ 𝐷 ) 𝑥 ) = ( ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ∘f ( +g ‘ 𝑅 ) 𝑥 ) )
43 3 6 20 36 5 39 41 lfladd0l ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ∘f ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 )
44 42 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) ( +g ‘ 𝐷 ) 𝑥 ) = 𝑥 )
45 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
46 eqid ⊢ ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) )
47 3 6 45 46 5 39 41 lflnegcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) ∈ 𝐹 )
48 5 6 20 1 15 39 47 41 ldualvadd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) ( +g ‘ 𝐷 ) 𝑥 ) = ( ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) ∘f ( +g ‘ 𝑅 ) 𝑥 ) )
49 3 6 45 46 5 39 41 20 36 lflnegl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) ∘f ( +g ‘ 𝑅 ) 𝑥 ) = ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) )
50 48 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐹 ) → ( ( 𝑧 ∈ 𝑉 ↦ ( ( invg ‘ 𝑅 ) ‘ ( 𝑥 ‘ 𝑧 ) ) ) ( +g ‘ 𝐷 ) 𝑥 ) = ( 𝑉 × { ( 0g ‘ 𝑅 ) } ) )
51 13 14 19 35 38 44 47 50 isgrpd ⊢ ( 𝜑 → 𝐷 ∈ Grp )