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

Proof

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

Metamath Proof Explorer

Theorem hdmapglem5

Proof