# 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 )