hdmapinvlem3

Description: Line 30 in Baer p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem3.h	$⊢ H = LHyp (K)$
	hdmapinvlem3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapinvlem3.o	$⊢ O = ocH (K) (W)$
	hdmapinvlem3.u	$⊢ U = DVecH (K) (W)$
	hdmapinvlem3.v	$⊢ V = {Base}_{U}$
	hdmapinvlem3.p	$⊢ \underset{˙}{+} = +_{U}$
	hdmapinvlem3.m	$⊢ \underset{˙}{-} = -_{U}$
	hdmapinvlem3.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmapinvlem3.r	$⊢ R = Scalar (U)$
	hdmapinvlem3.b	$⊢ B = {Base}_{R}$
	hdmapinvlem3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hdmapinvlem3.z	$⊢ \underset{˙}{0} = 0_{R}$
	hdmapinvlem3.s	$⊢ S = HDMap (K) (W)$
	hdmapinvlem3.g	$⊢ G = HGMap (K) (W)$
	hdmapinvlem3.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapinvlem3.c	$⊢ φ \to C \in O (\{E\})$
	hdmapinvlem3.d	$⊢ φ \to D \in O (\{E\})$
	hdmapinvlem3.i	$⊢ φ \to I \in B$
	hdmapinvlem3.j	$⊢ φ \to J \in B$
	hdmapinvlem3.ij	$⊢ φ \to I \underset{˙}{\times} G (J) = S (D) (C)$
Assertion	hdmapinvlem3	$⊢ φ \to S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem3.h	$⊢ H = LHyp (K)$
2		hdmapinvlem3.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapinvlem3.o	$⊢ O = ocH (K) (W)$
4		hdmapinvlem3.u	$⊢ U = DVecH (K) (W)$
5		hdmapinvlem3.v	$⊢ V = {Base}_{U}$
6		hdmapinvlem3.p	$⊢ \underset{˙}{+} = +_{U}$
7		hdmapinvlem3.m	$⊢ \underset{˙}{-} = -_{U}$
8		hdmapinvlem3.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
9		hdmapinvlem3.r	$⊢ R = Scalar (U)$
10		hdmapinvlem3.b	$⊢ B = {Base}_{R}$
11		hdmapinvlem3.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
12		hdmapinvlem3.z	$⊢ \underset{˙}{0} = 0_{R}$
13		hdmapinvlem3.s	$⊢ S = HDMap (K) (W)$
14		hdmapinvlem3.g	$⊢ G = HGMap (K) (W)$
15		hdmapinvlem3.k	$⊢ φ \to (K \in HL \land W \in H)$
16		hdmapinvlem3.c	$⊢ φ \to C \in O (\{E\})$
17		hdmapinvlem3.d	$⊢ φ \to D \in O (\{E\})$
18		hdmapinvlem3.i	$⊢ φ \to I \in B$
19		hdmapinvlem3.j	$⊢ φ \to J \in B$
20		hdmapinvlem3.ij	$⊢ φ \to I \underset{˙}{\times} G (J) = S (D) (C)$
21		eqid	$⊢ LCDual (K) (W) = LCDual (K) (W)$
22		eqid	$⊢ -_{LCDual (K) (W)} = -_{LCDual (K) (W)}$
23	1 4 15	dvhlmod	$⊢ φ \to U \in LMod$
24		eqid	$⊢ {Base}_{K} = {Base}_{K}$
25		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
26		eqid	$⊢ 0_{U} = 0_{U}$
27	1 24 25 4 5 26 2 15	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
28	27	eldifad	$⊢ φ \to E \in V$
29	5 9 8 10	lmodvscl	$⊢ (U \in LMod \land J \in B \land E \in V) \to J \underset{˙}{\cdot} E \in V$
30	23 19 28 29	syl3anc	$⊢ φ \to J \underset{˙}{\cdot} E \in V$
31	28	snssd	$⊢ φ \to \{E\} \subseteq V$
32	1 4 5 3	dochssv	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \subseteq V$
33	15 31 32	syl2anc	$⊢ φ \to O (\{E\}) \subseteq V$
34	33 17	sseldd	$⊢ φ \to D \in V$
35	1 4 5 7 21 22 13 15 30 34	hdmapsub	$⊢ φ \to S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) = S (J \underset{˙}{\cdot} E) -_{LCDual (K) (W)} S (D)$
36	35	fveq1d	$⊢ φ \to S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = (S (J \underset{˙}{\cdot} E) -_{LCDual (K) (W)} S (D)) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C)$
37		eqid	$⊢ -_{R} = -_{R}$
38		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
39	1 4 5 21 38 13 15 30	hdmapcl	$⊢ φ \to S (J \underset{˙}{\cdot} E) \in {Base}_{LCDual (K) (W)}$
40	1 4 5 21 38 13 15 34	hdmapcl	$⊢ φ \to S (D) \in {Base}_{LCDual (K) (W)}$
41	5 9 8 10	lmodvscl	$⊢ (U \in LMod \land I \in B \land E \in V) \to I \underset{˙}{\cdot} E \in V$
42	23 18 28 41	syl3anc	$⊢ φ \to I \underset{˙}{\cdot} E \in V$
43	33 16	sseldd	$⊢ φ \to C \in V$
44	5 6	lmodvacl	$⊢ (U \in LMod \land I \underset{˙}{\cdot} E \in V \land C \in V) \to (I \underset{˙}{\cdot} E) \underset{˙}{+} C \in V$
45	23 42 43 44	syl3anc	$⊢ φ \to (I \underset{˙}{\cdot} E) \underset{˙}{+} C \in V$
46	1 4 5 9 37 21 38 22 15 39 40 45	lcdvsubval	$⊢ φ \to (S (J \underset{˙}{\cdot} E) -_{LCDual (K) (W)} S (D)) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = S (J \underset{˙}{\cdot} E) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) -_{R} S (D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C)$
47		eqid	$⊢ +_{R} = +_{R}$
48	1 4 5 6 9 47 13 15 42 43 30	hdmaplna1	$⊢ φ \to S (J \underset{˙}{\cdot} E) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = S (J \underset{˙}{\cdot} E) (I \underset{˙}{\cdot} E) +_{R} S (J \underset{˙}{\cdot} E) (C)$
49	1 4 5 8 9 10 11 13 14 15 42 28 19	hdmapglnm2	$⊢ φ \to S (J \underset{˙}{\cdot} E) (I \underset{˙}{\cdot} E) = S (E) (I \underset{˙}{\cdot} E) \underset{˙}{\times} G (J)$
50	1 4 5 8 9 10 11 13 15 28 28 18	hdmaplnm1	$⊢ φ \to S (E) (I \underset{˙}{\cdot} E) = I \underset{˙}{\times} S (E) (E)$
51		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
52		eqid	$⊢ 1_{R} = 1_{R}$
53	1 2 51 13 15 4 9 52	hdmapevec2	$⊢ φ \to S (E) (E) = 1_{R}$
54	53	oveq2d	$⊢ φ \to I \underset{˙}{\times} S (E) (E) = I \underset{˙}{\times} 1_{R}$
55	9	lmodring	$⊢ U \in LMod \to R \in Ring$
56	23 55	syl	$⊢ φ \to R \in Ring$
57	10 11 52	ringridm	$⊢ (R \in Ring \land I \in B) \to I \underset{˙}{\times} 1_{R} = I$
58	56 18 57	syl2anc	$⊢ φ \to I \underset{˙}{\times} 1_{R} = I$
59	50 54 58	3eqtrd	$⊢ φ \to S (E) (I \underset{˙}{\cdot} E) = I$
60	59	oveq1d	$⊢ φ \to S (E) (I \underset{˙}{\cdot} E) \underset{˙}{\times} G (J) = I \underset{˙}{\times} G (J)$
61	49 60	eqtrd	$⊢ φ \to S (J \underset{˙}{\cdot} E) (I \underset{˙}{\cdot} E) = I \underset{˙}{\times} G (J)$
62	1 4 5 8 9 10 11 13 14 15 43 28 19	hdmapglnm2	$⊢ φ \to S (J \underset{˙}{\cdot} E) (C) = S (E) (C) \underset{˙}{\times} G (J)$
63	1 2 3 4 5 9 10 11 12 13 15 16	hdmapinvlem1	$⊢ φ \to S (E) (C) = \underset{˙}{0}$
64	63	oveq1d	$⊢ φ \to S (E) (C) \underset{˙}{\times} G (J) = \underset{˙}{0} \underset{˙}{\times} G (J)$
65	1 4 9 10 14 15 19	hgmapcl	$⊢ φ \to G (J) \in B$
66	10 11 12	ringlz	$⊢ (R \in Ring \land G (J) \in B) \to \underset{˙}{0} \underset{˙}{\times} G (J) = \underset{˙}{0}$
67	56 65 66	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\times} G (J) = \underset{˙}{0}$
68	62 64 67	3eqtrd	$⊢ φ \to S (J \underset{˙}{\cdot} E) (C) = \underset{˙}{0}$
69	61 68	oveq12d	$⊢ φ \to S (J \underset{˙}{\cdot} E) (I \underset{˙}{\cdot} E) +_{R} S (J \underset{˙}{\cdot} E) (C) = (I \underset{˙}{\times} G (J)) +_{R} \underset{˙}{0}$
70		ringgrp	$⊢ R \in Ring \to R \in Grp$
71	56 70	syl	$⊢ φ \to R \in Grp$
72	9 10 11	lmodmcl	$⊢ (U \in LMod \land I \in B \land G (J) \in B) \to I \underset{˙}{\times} G (J) \in B$
73	23 18 65 72	syl3anc	$⊢ φ \to I \underset{˙}{\times} G (J) \in B$
74	10 47 12	grprid	$⊢ (R \in Grp \land I \underset{˙}{\times} G (J) \in B) \to (I \underset{˙}{\times} G (J)) +_{R} \underset{˙}{0} = I \underset{˙}{\times} G (J)$
75	71 73 74	syl2anc	$⊢ φ \to (I \underset{˙}{\times} G (J)) +_{R} \underset{˙}{0} = I \underset{˙}{\times} G (J)$
76	48 69 75	3eqtrd	$⊢ φ \to S (J \underset{˙}{\cdot} E) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = I \underset{˙}{\times} G (J)$
77	1 4 5 6 9 47 13 15 42 43 34	hdmaplna1	$⊢ φ \to S (D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = S (D) (I \underset{˙}{\cdot} E) +_{R} S (D) (C)$
78	1 4 5 8 9 10 11 13 15 28 34 18	hdmaplnm1	$⊢ φ \to S (D) (I \underset{˙}{\cdot} E) = I \underset{˙}{\times} S (D) (E)$
79	1 2 3 4 5 9 10 11 12 13 15 17	hdmapinvlem2	$⊢ φ \to S (D) (E) = \underset{˙}{0}$
80	79	oveq2d	$⊢ φ \to I \underset{˙}{\times} S (D) (E) = I \underset{˙}{\times} \underset{˙}{0}$
81	10 11 12	ringrz	$⊢ (R \in Ring \land I \in B) \to I \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
82	56 18 81	syl2anc	$⊢ φ \to I \underset{˙}{\times} \underset{˙}{0} = \underset{˙}{0}$
83	78 80 82	3eqtrrd	$⊢ φ \to \underset{˙}{0} = S (D) (I \underset{˙}{\cdot} E)$
84	83 20	oveq12d	$⊢ φ \to \underset{˙}{0} +_{R} (I \underset{˙}{\times} G (J)) = S (D) (I \underset{˙}{\cdot} E) +_{R} S (D) (C)$
85	10 47 12	grplid	$⊢ (R \in Grp \land I \underset{˙}{\times} G (J) \in B) \to \underset{˙}{0} +_{R} (I \underset{˙}{\times} G (J)) = I \underset{˙}{\times} G (J)$
86	71 73 85	syl2anc	$⊢ φ \to \underset{˙}{0} +_{R} (I \underset{˙}{\times} G (J)) = I \underset{˙}{\times} G (J)$
87	77 84 86	3eqtr2d	$⊢ φ \to S (D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = I \underset{˙}{\times} G (J)$
88	76 87	oveq12d	$⊢ φ \to S (J \underset{˙}{\cdot} E) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) -_{R} S (D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = (I \underset{˙}{\times} G (J)) -_{R} (I \underset{˙}{\times} G (J))$
89	46 88	eqtrd	$⊢ φ \to (S (J \underset{˙}{\cdot} E) -_{LCDual (K) (W)} S (D)) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = (I \underset{˙}{\times} G (J)) -_{R} (I \underset{˙}{\times} G (J))$
90	10 12 37	grpsubid	$⊢ (R \in Grp \land I \underset{˙}{\times} G (J) \in B) \to (I \underset{˙}{\times} G (J)) -_{R} (I \underset{˙}{\times} G (J)) = \underset{˙}{0}$
91	71 73 90	syl2anc	$⊢ φ \to (I \underset{˙}{\times} G (J)) -_{R} (I \underset{˙}{\times} G (J)) = \underset{˙}{0}$
92	36 89 91	3eqtrd	$⊢ φ \to S ((J \underset{˙}{\cdot} E) \underset{˙}{-} D) ((I \underset{˙}{\cdot} E) \underset{˙}{+} C) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem hdmapinvlem3

Proof