mapdheq2

Description: Lemmma for ~? mapdh . One direction of part (2) in Baer p. 45. (Contributed by NM, 4-Apr-2015)

	Ref	Expression
Hypotheses	mapdh.q	$⊢ Q = 0_{C}$
	mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh.h	$⊢ H = LHyp (K)$
	mapdh.m	$⊢ M = mapd (K) (W)$
	mapdh.u	$⊢ U = DVecH (K) (W)$
	mapdh.v	$⊢ V = {Base}_{U}$
	mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
	mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
	mapdh.n	$⊢ N = LSpan (U)$
	mapdh.c	$⊢ C = LCDual (K) (W)$
	mapdh.d	$⊢ D = {Base}_{C}$
	mapdh.r	$⊢ R = -_{C}$
	mapdh.j	$⊢ J = LSpan (C)$
	mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdhc.f	$⊢ φ \to F \in D$
	mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
	mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	mapdhe.g	$⊢ φ \to G \in D$
	mapdh.ne2	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
Assertion	mapdheq2	$⊢ φ \to (I (⟨X, F, Y⟩) = G \to I (⟨Y, G, X⟩) = F)$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$⊢ Q = 0_{C}$
2		mapdh.i	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
3		mapdh.h	$⊢ H = LHyp (K)$
4		mapdh.m	$⊢ M = mapd (K) (W)$
5		mapdh.u	$⊢ U = DVecH (K) (W)$
6		mapdh.v	$⊢ V = {Base}_{U}$
7		mapdh.s	$⊢ \underset{˙}{-} = -_{U}$
8		mapdhc.o	$⊢ \underset{˙}{0} = 0_{U}$
9		mapdh.n	$⊢ N = LSpan (U)$
10		mapdh.c	$⊢ C = LCDual (K) (W)$
11		mapdh.d	$⊢ D = {Base}_{C}$
12		mapdh.r	$⊢ R = -_{C}$
13		mapdh.j	$⊢ J = LSpan (C)$
14		mapdh.k	$⊢ φ \to (K \in HL \land W \in H)$
15		mapdhc.f	$⊢ φ \to F \in D$
16		mapdh.mn	$⊢ φ \to M (N (\{X\})) = J (\{F\})$
17		mapdhcl.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
18		mapdhe.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
19		mapdhe.g	$⊢ φ \to G \in D$
20		mapdh.ne2	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	mapdheq	$⊢ φ \to (I (⟨X, F, Y⟩) = G \leftrightarrow (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})))$
22	16	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to M (N (\{X\})) = J (\{F\})$
23	3 5 14	dvhlmod	$⊢ φ \to U \in LMod$
24	17	eldifad	$⊢ φ \to X \in V$
25	18	eldifad	$⊢ φ \to Y \in V$
26	6 7 9 23 24 25	lspsnsub	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) = N (\{Y \underset{˙}{-} X\})$
27	26	fveq2d	$⊢ φ \to M (N (\{X \underset{˙}{-} Y\})) = M (N (\{Y \underset{˙}{-} X\}))$
28	3 10 14	lcdlmod	$⊢ φ \to C \in LMod$
29	11 12 13 28 15 19	lspsnsub	$⊢ φ \to J (\{F R G\}) = J (\{G R F\})$
30	27 29	eqeq12d	$⊢ φ \to (M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}) \leftrightarrow M (N (\{Y \underset{˙}{-} X\})) = J (\{G R F\}))$
31	30	biimpa	$⊢ (φ \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})) \to M (N (\{Y \underset{˙}{-} X\})) = J (\{G R F\})$
32	31	adantrl	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to M (N (\{Y \underset{˙}{-} X\})) = J (\{G R F\})$
33	14	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to (K \in HL \land W \in H)$
34	19	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to G \in D$
35		simprl	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to M (N (\{Y\})) = J (\{G\})$
36	18	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to Y \in (V ∖ \{\underset{˙}{0}\})$
37	17	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to X \in (V ∖ \{\underset{˙}{0}\})$
38	15	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to F \in D$
39	20	necomd	$⊢ φ \to N (\{Y\}) \neq N (\{X\})$
40	39	adantr	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to N (\{Y\}) \neq N (\{X\})$
41	1 2 3 4 5 6 7 8 9 10 11 12 13 33 34 35 36 37 38 40	mapdheq	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to (I (⟨Y, G, X⟩) = F \leftrightarrow (M (N (\{X\})) = J (\{F\}) \land M (N (\{Y \underset{˙}{-} X\})) = J (\{G R F\})))$
42	22 32 41	mpbir2and	$⊢ (φ \land (M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\}))) \to I (⟨Y, G, X⟩) = F$
43	42	ex	$⊢ φ \to ((M (N (\{Y\})) = J (\{G\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R G\})) \to I (⟨Y, G, X⟩) = F)$
44	21 43	sylbid	$⊢ φ \to (I (⟨X, F, Y⟩) = G \to I (⟨Y, G, X⟩) = F)$

Metamath Proof Explorer

Theorem mapdheq2

Proof