hgmapvvlem3

Description: Lemma for hgmapvv . Eliminate ( ( SD )C ) = .1. (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015)

	Ref	Expression
Hypotheses	hdmapglem6.h	$⊢ H = LHyp (K)$
	hdmapglem6.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
	hdmapglem6.o	$⊢ O = ocH (K) (W)$
	hdmapglem6.u	$⊢ U = DVecH (K) (W)$
	hdmapglem6.v	$⊢ V = {Base}_{U}$
	hdmapglem6.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmapglem6.r	$⊢ R = Scalar (U)$
	hdmapglem6.b	$⊢ B = {Base}_{R}$
	hdmapglem6.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hdmapglem6.z	$⊢ \underset{˙}{0} = 0_{R}$
	hdmapglem6.i	$⊢ \underset{˙}{1} = 1_{R}$
	hdmapglem6.n	$⊢ N = {inv}_{r} (R)$
	hdmapglem6.s	$⊢ S = HDMap (K) (W)$
	hdmapglem6.g	$⊢ G = HGMap (K) (W)$
	hdmapglem6.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapglem6.x	$⊢ φ \to X \in (B ∖ \{\underset{˙}{0}\})$
Assertion	hgmapvvlem3	$⊢ φ \to G (G (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		hdmapglem6.h	$⊢ H = LHyp (K)$
2		hdmapglem6.e	$⊢ E = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
3		hdmapglem6.o	$⊢ O = ocH (K) (W)$
4		hdmapglem6.u	$⊢ U = DVecH (K) (W)$
5		hdmapglem6.v	$⊢ V = {Base}_{U}$
6		hdmapglem6.q	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		hdmapglem6.r	$⊢ R = Scalar (U)$
8		hdmapglem6.b	$⊢ B = {Base}_{R}$
9		hdmapglem6.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
10		hdmapglem6.z	$⊢ \underset{˙}{0} = 0_{R}$
11		hdmapglem6.i	$⊢ \underset{˙}{1} = 1_{R}$
12		hdmapglem6.n	$⊢ N = {inv}_{r} (R)$
13		hdmapglem6.s	$⊢ S = HDMap (K) (W)$
14		hdmapglem6.g	$⊢ G = HGMap (K) (W)$
15		hdmapglem6.k	$⊢ φ \to (K \in HL \land W \in H)$
16		hdmapglem6.x	$⊢ φ \to X \in (B ∖ \{\underset{˙}{0}\})$
17		eqid	$⊢ 0_{U} = 0_{U}$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
20	1 18 19 4 5 17 2 15	dvheveccl	$⊢ φ \to E \in (V ∖ \{0_{U}\})$
21	20	eldifad	$⊢ φ \to E \in V$
22	1 3 4 5 17 15 21	dochsnnz	$⊢ φ \to O (\{E\}) \neq \{0_{U}\}$
23	21	snssd	$⊢ φ \to \{E\} \subseteq V$
24		eqid	$⊢ LSubSp (U) = LSubSp (U)$
25	1 4 5 24 3	dochlss	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \in LSubSp (U)$
26	15 23 25	syl2anc	$⊢ φ \to O (\{E\}) \in LSubSp (U)$
27	17 24	lssne0	$⊢ O (\{E\}) \in LSubSp (U) \to (O (\{E\}) \neq \{0_{U}\} \leftrightarrow \exists k \in O (\{E\}) k \neq 0_{U})$
28	26 27	syl	$⊢ φ \to (O (\{E\}) \neq \{0_{U}\} \leftrightarrow \exists k \in O (\{E\}) k \neq 0_{U})$
29	22 28	mpbid	$⊢ φ \to \exists k \in O (\{E\}) k \neq 0_{U}$
30		eqid	$⊢ \cdot_{U} = \cdot_{U}$
31	15	3ad2ant1	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to (K \in HL \land W \in H)$
32	1 4 5 3	dochssv	$⊢ ((K \in HL \land W \in H) \land \{E\} \subseteq V) \to O (\{E\}) \subseteq V$
33	15 23 32	syl2anc	$⊢ φ \to O (\{E\}) \subseteq V$
34	33	sselda	$⊢ (φ \land k \in O (\{E\})) \to k \in V$
35	34	3adant3	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to k \in V$
36		simp3	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to k \neq 0_{U}$
37		eldifsn	$⊢ k \in (V ∖ \{0_{U}\}) \leftrightarrow (k \in V \land k \neq 0_{U})$
38	35 36 37	sylanbrc	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to k \in (V ∖ \{0_{U}\})$
39		eqid	$⊢ N (S (k) (k)) \cdot_{U} k = N (S (k) (k)) \cdot_{U} k$
40	1 4 5 30 17 7 11 12 13 31 38 39	hdmapip1	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}$
41		simpl1	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to φ$
42	41 15	syl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to (K \in HL \land W \in H)$
43	41 16	syl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to X \in (B ∖ \{\underset{˙}{0}\})$
44	1 4 15	dvhlmod	$⊢ φ \to U \in LMod$
45	41 44	syl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to U \in LMod$
46	41 26	syl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to O (\{E\}) \in LSubSp (U)$
47	1 4 15	dvhlvec	$⊢ φ \to U \in LVec$
48	7	lvecdrng	$⊢ U \in LVec \to R \in DivRing$
49	47 48	syl	$⊢ φ \to R \in DivRing$
50	41 49	syl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to R \in DivRing$
51	35	adantr	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to k \in V$
52	1 4 5 7 8 13 42 51 51	hdmapipcl	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to S (k) (k) \in B$
53	15	adantr	$⊢ (φ \land k \in O (\{E\})) \to (K \in HL \land W \in H)$
54	1 4 5 17 7 10 13 53 34	hdmapip0	$⊢ (φ \land k \in O (\{E\})) \to (S (k) (k) = \underset{˙}{0} \leftrightarrow k = 0_{U})$
55	54	necon3bid	$⊢ (φ \land k \in O (\{E\})) \to (S (k) (k) \neq \underset{˙}{0} \leftrightarrow k \neq 0_{U})$
56	55	biimp3ar	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to S (k) (k) \neq \underset{˙}{0}$
57	56	adantr	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to S (k) (k) \neq \underset{˙}{0}$
58	8 10 12	drnginvrcl	$⊢ (R \in DivRing \land S (k) (k) \in B \land S (k) (k) \neq \underset{˙}{0}) \to N (S (k) (k)) \in B$
59	50 52 57 58	syl3anc	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to N (S (k) (k)) \in B$
60		simpl2	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to k \in O (\{E\})$
61	7 30 8 24	lssvscl	$⊢ ((U \in LMod \land O (\{E\}) \in LSubSp (U)) \land (N (S (k) (k)) \in B \land k \in O (\{E\}))) \to N (S (k) (k)) \cdot_{U} k \in O (\{E\})$
62	45 46 59 60 61	syl22anc	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to N (S (k) (k)) \cdot_{U} k \in O (\{E\})$
63		simpr	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}$
64	1 2 3 4 5 6 7 8 9 10 11 12 13 14 42 43 62 60 63	hgmapvvlem2	$⊢ ((φ \land k \in O (\{E\}) \land k \neq 0_{U}) \land S (k) (N (S (k) (k)) \cdot_{U} k) = \underset{˙}{1}) \to G (G (X)) = X$
65	40 64	mpdan	$⊢ (φ \land k \in O (\{E\}) \land k \neq 0_{U}) \to G (G (X)) = X$
66	65	rexlimdv3a	$⊢ φ \to (\exists k \in O (\{E\}) k \neq 0_{U} \to G (G (X)) = X)$
67	29 66	mpd	$⊢ φ \to G (G (X)) = X$

Metamath Proof Explorer

Theorem hgmapvvlem3

Proof