hdmap14lem12

Description: Lemma for proof of part 14 in Baer p. 50. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem12.h	$⊢ H = LHyp (K)$
	hdmap14lem12.u	$⊢ U = DVecH (K) (W)$
	hdmap14lem12.v	$⊢ V = {Base}_{U}$
	hdmap14lem12.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hdmap14lem12.r	$⊢ R = Scalar (U)$
	hdmap14lem12.b	$⊢ B = {Base}_{R}$
	hdmap14lem12.c	$⊢ C = LCDual (K) (W)$
	hdmap14lem12.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
	hdmap14lem12.s	$⊢ S = HDMap (K) (W)$
	hdmap14lem12.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmap14lem12.f	$⊢ φ \to F \in B$
	hdmap14lem12.p	$⊢ P = Scalar (C)$
	hdmap14lem12.a	$⊢ A = {Base}_{P}$
	hdmap14lem12.o	$⊢ \underset{˙}{0} = 0_{U}$
	hdmap14lem12.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hdmap14lem12.g	$⊢ φ \to G \in A$
Assertion	hdmap14lem12	$⊢ φ \to (S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \leftrightarrow \forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y))$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	$⊢ H = LHyp (K)$
2		hdmap14lem12.u	$⊢ U = DVecH (K) (W)$
3		hdmap14lem12.v	$⊢ V = {Base}_{U}$
4		hdmap14lem12.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
5		hdmap14lem12.r	$⊢ R = Scalar (U)$
6		hdmap14lem12.b	$⊢ B = {Base}_{R}$
7		hdmap14lem12.c	$⊢ C = LCDual (K) (W)$
8		hdmap14lem12.e	$⊢ \underset{˙}{∙} = \cdot_{C}$
9		hdmap14lem12.s	$⊢ S = HDMap (K) (W)$
10		hdmap14lem12.k	$⊢ φ \to (K \in HL \land W \in H)$
11		hdmap14lem12.f	$⊢ φ \to F \in B$
12		hdmap14lem12.p	$⊢ P = Scalar (C)$
13		hdmap14lem12.a	$⊢ A = {Base}_{P}$
14		hdmap14lem12.o	$⊢ \underset{˙}{0} = 0_{U}$
15		hdmap14lem12.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
16		hdmap14lem12.g	$⊢ φ \to G \in A$
17		eqid	$⊢ LSpan (C) = LSpan (C)$
18	10	3ad2ant1	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to (K \in HL \land W \in H)$
19		simp3	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to y \in (V ∖ \{\underset{˙}{0}\})$
20	19	eldifad	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to y \in V$
21	11	3ad2ant1	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to F \in B$
22	1 2 3 4 5 6 7 8 17 12 13 9 18 20 21	hdmap14lem2a	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to \exists g \in A S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)$
23		simp3	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)$
24		eqid	$⊢ +_{U} = +_{U}$
25		eqid	$⊢ LSpan (U) = LSpan (U)$
26		eqid	$⊢ +_{C} = +_{C}$
27		simp11	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to φ$
28	27 10	syl	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to (K \in HL \land W \in H)$
29	27 15	syl	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to X \in (V ∖ \{\underset{˙}{0}\})$
30		simp13	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to y \in (V ∖ \{\underset{˙}{0}\})$
31	27 11	syl	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to F \in B$
32	27 16	syl	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to G \in A$
33		simp2	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to g \in A$
34		simp12	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
35	1 2 3 24 4 14 25 5 6 7 26 8 12 13 9 28 29 30 31 32 33 34 23	hdmap14lem11	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to G = g$
36	35	oveq1d	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to G \underset{˙}{∙} S (y) = g \underset{˙}{∙} S (y)$
37	23 36	eqtr4d	$⊢ ((φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \land g \in A \land S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y)) \to S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y)$
38	37	rexlimdv3a	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to (\exists g \in A S (F \underset{˙}{\cdot} y) = g \underset{˙}{∙} S (y) \to S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y))$
39	22 38	mpd	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \land y \in (V ∖ \{\underset{˙}{0}\})) \to S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y)$
40	39	3expia	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)) \to (y \in (V ∖ \{\underset{˙}{0}\}) \to S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y))$
41	40	ralrimiv	$⊢ (φ \land S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)) \to \forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y)$
42		oveq2	$⊢ y = X \to F \underset{˙}{\cdot} y = F \underset{˙}{\cdot} X$
43	42	fveq2d	$⊢ y = X \to S (F \underset{˙}{\cdot} y) = S (F \underset{˙}{\cdot} X)$
44		fveq2	$⊢ y = X \to S (y) = S (X)$
45	44	oveq2d	$⊢ y = X \to G \underset{˙}{∙} S (y) = G \underset{˙}{∙} S (X)$
46	43 45	eqeq12d	$⊢ y = X \to (S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y) \leftrightarrow S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X))$
47	46	rspcv	$⊢ X \in (V ∖ \{\underset{˙}{0}\}) \to (\forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X))$
48	15 47	syl	$⊢ φ \to (\forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X))$
49	48	imp	$⊢ (φ \land \forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y)) \to S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X)$
50	41 49	impbida	$⊢ φ \to (S (F \underset{˙}{\cdot} X) = G \underset{˙}{∙} S (X) \leftrightarrow \forall y \in (V ∖ \{\underset{˙}{0}\}) S (F \underset{˙}{\cdot} y) = G \underset{˙}{∙} S (y))$

Metamath Proof Explorer

Theorem hdmap14lem12

Proof