ldualgrplem

	Ref	Expression
Hypotheses	ldualgrp.d	$⊢ D = LDual (W)$
	ldualgrp.w	$⊢ φ \to W \in LMod$
	ldualgrp.v	$⊢ V = {Base}_{W}$
	ldualgrp.p	$⊢ \underset{˙}{+} = \circ_{f} +_{W}$
	ldualgrp.f	$⊢ F = LFnl (W)$
	ldualgrp.r	$⊢ R = Scalar (W)$
	ldualgrp.k	$⊢ K = {Base}_{R}$
	ldualgrp.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	ldualgrp.o	$⊢ O = {opp}_{r} (R)$
	ldualgrp.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
Assertion	ldualgrplem	$⊢ φ \to D \in Grp$

Proof

Step	Hyp	Ref	Expression
1		ldualgrp.d	$⊢ D = LDual (W)$
2		ldualgrp.w	$⊢ φ \to W \in LMod$
3		ldualgrp.v	$⊢ V = {Base}_{W}$
4		ldualgrp.p	$⊢ \underset{˙}{+} = \circ_{f} +_{W}$
5		ldualgrp.f	$⊢ F = LFnl (W)$
6		ldualgrp.r	$⊢ R = Scalar (W)$
7		ldualgrp.k	$⊢ K = {Base}_{R}$
8		ldualgrp.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
9		ldualgrp.o	$⊢ O = {opp}_{r} (R)$
10		ldualgrp.s	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
11		eqid	$⊢ {Base}_{D} = {Base}_{D}$
12	5 1 11 2	ldualvbase	$⊢ φ \to {Base}_{D} = F$
13	12	eqcomd	$⊢ φ \to F = {Base}_{D}$
14		eqidd	$⊢ φ \to +_{D} = +_{D}$
15		eqid	$⊢ +_{D} = +_{D}$
16	2	3ad2ant1	$⊢ (φ \land x \in F \land y \in F) \to W \in LMod$
17		simp2	$⊢ (φ \land x \in F \land y \in F) \to x \in F$
18		simp3	$⊢ (φ \land x \in F \land y \in F) \to y \in F$
19	5 1 15 16 17 18	ldualvaddcl	$⊢ (φ \land x \in F \land y \in F) \to x +_{D} y \in F$
20		eqid	$⊢ +_{R} = +_{R}$
21	2	adantr	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to W \in LMod$
22		simpr2	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to y \in F$
23		simpr3	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to z \in F$
24	5 6 20 1 15 21 22 23	ldualvadd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to y +_{D} z = y {+_{R}}_{f} z$
25	24	oveq2d	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to x {+_{R}}_{f} (y +_{D} z) = x {+_{R}}_{f} (y {+_{R}}_{f} z)$
26		simpr1	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to x \in F$
27	5 1 15 21 22 23	ldualvaddcl	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to y +_{D} z \in F$
28	5 6 20 1 15 21 26 27	ldualvadd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to x +_{D} (y +_{D} z) = x {+_{R}}_{f} (y +_{D} z)$
29	5 1 15 21 26 22	ldualvaddcl	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to x +_{D} y \in F$
30	5 6 20 1 15 21 29 23	ldualvadd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to (x +_{D} y) +_{D} z = (x +_{D} y) {+_{R}}_{f} z$
31	5 6 20 1 15 21 26 22	ldualvadd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to x +_{D} y = x {+_{R}}_{f} y$
32	31	oveq1d	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to (x +_{D} y) {+_{R}}_{f} z = (x {+_{R}}_{f} y) {+_{R}}_{f} z$
33	6 20 5 21 26 22 23	lfladdass	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to (x {+_{R}}_{f} y) {+_{R}}_{f} z = x {+_{R}}_{f} (y {+_{R}}_{f} z)$
34	30 32 33	3eqtrd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to (x +_{D} y) +_{D} z = x {+_{R}}_{f} (y {+_{R}}_{f} z)$
35	25 28 34	3eqtr4rd	$⊢ (φ \land (x \in F \land y \in F \land z \in F)) \to (x +_{D} y) +_{D} z = x +_{D} (y +_{D} z)$
36		eqid	$⊢ 0_{R} = 0_{R}$
37	6 36 3 5	lfl0f	$⊢ W \in LMod \to V \times \{0_{R}\} \in F$
38	2 37	syl	$⊢ φ \to V \times \{0_{R}\} \in F$
39	2	adantr	$⊢ (φ \land x \in F) \to W \in LMod$
40	38	adantr	$⊢ (φ \land x \in F) \to V \times \{0_{R}\} \in F$
41		simpr	$⊢ (φ \land x \in F) \to x \in F$
42	5 6 20 1 15 39 40 41	ldualvadd	$⊢ (φ \land x \in F) \to (V \times \{0_{R}\}) +_{D} x = (V \times \{0_{R}\}) {+_{R}}_{f} x$
43	3 6 20 36 5 39 41	lfladd0l	$⊢ (φ \land x \in F) \to (V \times \{0_{R}\}) {+_{R}}_{f} x = x$
44	42 43	eqtrd	$⊢ (φ \land x \in F) \to (V \times \{0_{R}\}) +_{D} x = x$
45		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
46		eqid	$⊢ (z \in V ⟼ {inv}_{g} (R) (x (z))) = (z \in V ⟼ {inv}_{g} (R) (x (z)))$
47	3 6 45 46 5 39 41	lflnegcl	$⊢ (φ \land x \in F) \to (z \in V ⟼ {inv}_{g} (R) (x (z))) \in F$
48	5 6 20 1 15 39 47 41	ldualvadd	$⊢ (φ \land x \in F) \to (z \in V ⟼ {inv}_{g} (R) (x (z))) +_{D} x = (z \in V ⟼ {inv}_{g} (R) (x (z))) {+_{R}}_{f} x$
49	3 6 45 46 5 39 41 20 36	lflnegl	$⊢ (φ \land x \in F) \to (z \in V ⟼ {inv}_{g} (R) (x (z))) {+_{R}}_{f} x = V \times \{0_{R}\}$
50	48 49	eqtrd	$⊢ (φ \land x \in F) \to (z \in V ⟼ {inv}_{g} (R) (x (z))) +_{D} x = V \times \{0_{R}\}$
51	13 14 19 35 38 44 47 50	isgrpd	$⊢ φ \to D \in Grp$

Metamath Proof Explorer

Theorem ldualgrplem

Proof