Theorem hdmapinvlem4

Description: Part 1.1 of Proposition 1 of Baer p. 110. We use C , D , I , and J for Baer's u, v, s, and t. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SD )C ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapinvlem3.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapinvlem3.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapinvlem3.p	⊢ + = ( +g ‘ 𝑈 )
	hdmapinvlem3.m	⊢ − = ( -g ‘ 𝑈 )
	hdmapinvlem3.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
	hdmapinvlem3.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapinvlem3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapinvlem3.t	⊢ × = ( .r ‘ 𝑅 )
	hdmapinvlem3.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapinvlem3.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem3.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapinvlem3.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
	hdmapinvlem3.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
	hdmapinvlem3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
	hdmapinvlem3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
	hdmapinvlem3.ij	⊢ ( 𝜑 → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
Assertion	hdmapinvlem4	⊢ ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapinvlem3.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapinvlem3.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapinvlem3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapinvlem3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		hdmapinvlem3.p	⊢ + = ( +g ‘ 𝑈 )
7		hdmapinvlem3.m	⊢ − = ( -g ‘ 𝑈 )
8		hdmapinvlem3.q	⊢ · = ( ·𝑠 ‘ 𝑈 )
9		hdmapinvlem3.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
10		hdmapinvlem3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
11		hdmapinvlem3.t	⊢ × = ( .r ‘ 𝑅 )
12		hdmapinvlem3.z	⊢ 0 = ( 0g ‘ 𝑅 )
13		hdmapinvlem3.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
14		hdmapinvlem3.g	⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
15		hdmapinvlem3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16		hdmapinvlem3.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
17		hdmapinvlem3.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
18		hdmapinvlem3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
19		hdmapinvlem3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
20		hdmapinvlem3.ij	⊢ ( 𝜑 → ( 𝐼 × ( 𝐺 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
21		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
22	1 4 15	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
25		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
26	1 23 24 4 5 25 2 15	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
27	26	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
28	5 9 8 10	lmodvscl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
29	22 19 27 28	syl3anc	⊢ ( 𝜑 → ( 𝐽 · 𝐸 ) ∈ 𝑉 )
30	27	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
31	1 4 5 3	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
32	15 30 31	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
33	32 17	sseldd	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
34	5 9 8 10	lmodvscl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐼 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
35	22 18 27 34	syl3anc	⊢ ( 𝜑 → ( 𝐼 · 𝐸 ) ∈ 𝑉 )
36	32 16	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
37	5 6	lmodvacl	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐼 · 𝐸 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
38	22 35 36 37	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 · 𝐸 ) + 𝐶 ) ∈ 𝑉 )
39	1 4 5 7 9 21 13 15 29 33 38	hdmaplns1	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = ( ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) ) )
40	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	hdmapinvlem3	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 )
41	5 7	lmodvsubcl	⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝐽 · 𝐸 ) ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝐽 · 𝐸 ) − 𝐷 ) ∈ 𝑉 )
42	22 29 33 41	syl3anc	⊢ ( 𝜑 → ( ( 𝐽 · 𝐸 ) − 𝐷 ) ∈ 𝑉 )
43	1 4 5 9 12 13 15 42 38	hdmapip0com	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) = 0 ↔ ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = 0 ) )
44	40 43	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( ( 𝐽 · 𝐸 ) − 𝐷 ) ) = 0 )
45	1 4 5 8 9 10 11 13 15 27 38 19	hdmaplnm1	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) = ( 𝐽 × ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) ) )
46		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
47	1 4 5 6 9 46 13 15 27 35 36	hdmaplna2	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
48	1 2 3 4 5 9 10 11 12 13 15 16	hdmapinvlem2	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = 0 )
49	48	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) )
50	9	lmodring	⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
51	22 50	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
52		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
53	51 52	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
54	1 4 5 9 10 13 15 27 35	hdmapipcl	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ∈ 𝐵 )
55	10 46 12	grprid	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ∈ 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) )
56	53 54 55	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) )
57	1 4 5 8 9 10 11 13 14 15 27 27 18	hdmapglnm2	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) )
58		eqid	⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
59		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
60	1 2 58 13 15 4 9 59	hdmapevec2	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = ( 1r ‘ 𝑅 ) )
61	60	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) = ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) )
62	1 4 9 10 14 15 18	hgmapcl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 )
63	10 11 59	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
64	51 62 63	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
65	61 64	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 𝐺 ‘ 𝐼 ) )
66	56 57 65	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐸 ) ( +g ‘ 𝑅 ) 0 ) = ( 𝐺 ‘ 𝐼 ) )
67	47 49 66	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) = ( 𝐺 ‘ 𝐼 ) )
68	67	oveq2d	⊢ ( 𝜑 → ( 𝐽 × ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐸 ) ) = ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) )
69	45 68	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) = ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) )
70	1 4 5 6 9 46 13 15 33 35 36	hdmaplna2	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) = ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
71	1 4 5 8 9 10 11 13 14 15 33 27 18	hdmapglnm2	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) = ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) × ( 𝐺 ‘ 𝐼 ) ) )
72	1 2 3 4 5 9 10 11 12 13 15 17	hdmapinvlem1	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) = 0 )
73	72	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐷 ) × ( 𝐺 ‘ 𝐼 ) ) = ( 0 × ( 𝐺 ‘ 𝐼 ) ) )
74	10 11 12	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( 0 × ( 𝐺 ‘ 𝐼 ) ) = 0 )
75	51 62 74	syl2anc	⊢ ( 𝜑 → ( 0 × ( 𝐺 ‘ 𝐼 ) ) = 0 )
76	71 73 75	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) = 0 )
77	76	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐼 · 𝐸 ) ) ‘ 𝐷 ) ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
78	1 4 5 9 10 13 15 33 36	hdmapipcl	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 )
79	10 46 12	grplid	⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
80	53 78 79	syl2anc	⊢ ( 𝜑 → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
81	70 77 80	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
82	69 81	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ ( 𝐽 · 𝐸 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ ( ( 𝐼 · 𝐸 ) + 𝐶 ) ) ‘ 𝐷 ) ) = ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
83	39 44 82	3eqtr3rd	⊢ ( 𝜑 → ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 )
84	9 10 11	lmodmcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐽 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐵 ) → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 )
85	22 19 62 84	syl3anc	⊢ ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 )
86	10 12 21	grpsubeq0	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ∈ 𝐵 ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ∈ 𝐵 ) → ( ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 ↔ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
87	53 85 78 86	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) ( -g ‘ 𝑅 ) ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) = 0 ↔ ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) ) )
88	83 87	mpbid	⊢ ( 𝜑 → ( 𝐽 × ( 𝐺 ‘ 𝐼 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )