Theorem hdmapglem5

Description: Part 1.2 in Baer p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapglem5.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapglem5.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapglem5.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapglem5.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapglem5.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmapglem5.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	hdmapglem5.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmapglem5.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapglem5.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapglem5.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	hdmapglem5.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapglem5.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapglem5.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hdmapglem5.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapglem5.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
	hdmapglem5.d	$$⊢\phi \to D\in O\left(\left\{E\right\}\right)$$
	hdmapglem5.i	$$⊢\phi \to I\in B$$
	hdmapglem5.j	$$⊢\phi \to J\in B$$
Assertion	hdmapglem5	$$⊢\phi \to G\left(S\left(D\right)\left(C\right)\right)=S\left(C\right)\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem5.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapglem5.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapglem5.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hdmapglem5.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hdmapglem5.v	$$⊢V={\mathrm{Base}}_U$$
6		hdmapglem5.p	$$⊢\underset{\dot{}}{+}={+}_U$$
7		hdmapglem5.m	$$⊢\underset{\dot{}}{-}={-}_U$$
8		hdmapglem5.q	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
9		hdmapglem5.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
10		hdmapglem5.b	$$⊢B={\mathrm{Base}}_R$$
11		hdmapglem5.t	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
12		hdmapglem5.z	$$⊢\underset{\dot{}}{0}=0_R$$
13		hdmapglem5.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
14		hdmapglem5.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
15		hdmapglem5.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
16		hdmapglem5.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
17		hdmapglem5.d	$$⊢\phi \to D\in O\left(\left\{E\right\}\right)$$
18		hdmapglem5.i	$$⊢\phi \to I\in B$$
19		hdmapglem5.j	$$⊢\phi \to J\in B$$
20	1 4 15	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
21	9	lmodring	$$⊢U\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
22	20 21	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
23		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
24		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
25		eqid	$$⊢0_U=0_U$$
26	1 23 24 4 5 25 2 15	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
27	26	eldifad	$$⊢\phi \to E\in V$$
28	27	snssd	$$⊢\phi \to \left\{E\right\}\subseteq V$$
29	1 4 5 3	dochssv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{E\right\}\subseteq V\right)\to O\left(\left\{E\right\}\right)\subseteq V$$
30	15 28 29	syl2anc	$$⊢\phi \to O\left(\left\{E\right\}\right)\subseteq V$$
31	30 16	sseldd	$$⊢\phi \to C\in V$$
32	30 17	sseldd	$$⊢\phi \to D\in V$$
33	1 4 5 9 10 13 15 31 32	hdmapipcl	$$⊢\phi \to S\left(D\right)\left(C\right)\in B$$
34	1 4 9 10 14 15 33	hgmapcl	$$⊢\phi \to G\left(S\left(D\right)\left(C\right)\right)\in B$$
35		eqid	$$⊢1_R=1_R$$
36	10 11 35	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge G\left(S\left(D\right)\left(C\right)\right)\in B\right)\to 1_R\underset{\dot{}}{\times }G\left(S\left(D\right)\left(C\right)\right)=G\left(S\left(D\right)\left(C\right)\right)$$
37	22 34 36	syl2anc	$$⊢\phi \to 1_R\underset{\dot{}}{\times }G\left(S\left(D\right)\left(C\right)\right)=G\left(S\left(D\right)\left(C\right)\right)$$
38	10 35	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in B$$
39	22 38	syl	$$⊢\phi \to 1_R\in B$$
40	1 4 9 35 14 15	hgmapval1	$$⊢\phi \to G\left(1_R\right)=1_R$$
41	40	oveq2d	$$⊢\phi \to S\left(D\right)\left(C\right)\underset{\dot{}}{\times }G\left(1_R\right)=S\left(D\right)\left(C\right)\underset{\dot{}}{\times }{1}_R$$
42	10 11 35	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge S\left(D\right)\left(C\right)\in B\right)\to S\left(D\right)\left(C\right)\underset{\dot{}}{\times }{1}_R=S\left(D\right)\left(C\right)$$
43	22 33 42	syl2anc	$$⊢\phi \to S\left(D\right)\left(C\right)\underset{\dot{}}{\times }{1}_R=S\left(D\right)\left(C\right)$$
44	41 43	eqtrd	$$⊢\phi \to S\left(D\right)\left(C\right)\underset{\dot{}}{\times }G\left(1_R\right)=S\left(D\right)\left(C\right)$$
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 33 39 44	hdmapinvlem4	$$⊢\phi \to 1_R\underset{\dot{}}{\times }G\left(S\left(D\right)\left(C\right)\right)=S\left(C\right)\left(D\right)$$
46	37 45	eqtr3d	$$⊢\phi \to G\left(S\left(D\right)\left(C\right)\right)=S\left(C\right)\left(D\right)$$