diclspsn

Description: The value of isomorphism C is spanned by vector F . Part of proof of Lemma N of Crawley p. 121 line 29. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	diclspsn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diclspsn.a	$⊢ A = Atoms (K)$
	diclspsn.h	$⊢ H = LHyp (K)$
	diclspsn.p	$⊢ P = oc (K) (W)$
	diclspsn.t	$⊢ T = LTrn (K) (W)$
	diclspsn.i	$⊢ I = DIsoC (K) (W)$
	diclspsn.u	$⊢ U = DVecH (K) (W)$
	diclspsn.n	$⊢ N = LSpan (U)$
	diclspsn.f	$⊢ F = (ι f \in T \| f (P) = Q)$
Assertion	diclspsn	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = N (\{⟨F, {I ↾}_{T}⟩\})$

Proof

Step	Hyp	Ref	Expression
1		diclspsn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		diclspsn.a	$⊢ A = Atoms (K)$
3		diclspsn.h	$⊢ H = LHyp (K)$
4		diclspsn.p	$⊢ P = oc (K) (W)$
5		diclspsn.t	$⊢ T = LTrn (K) (W)$
6		diclspsn.i	$⊢ I = DIsoC (K) (W)$
7		diclspsn.u	$⊢ U = DVecH (K) (W)$
8		diclspsn.n	$⊢ N = LSpan (U)$
9		diclspsn.f	$⊢ F = (ι f \in T \| f (P) = Q)$
10		df-rab	$⊢ \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} = \{v \| (v \in (T \times TEndo (K) (W)) \land \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)\}$
11		relopabv	$⊢ Rel \{⟨y, z⟩ \| (y = z (F) \land z \in TEndo (K) (W))\}$
12		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
13	1 2 3 4 5 12 6 9	dicval2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{⟨y, z⟩ \| (y = z (F) \land z \in TEndo (K) (W))\}$
14	13	releqd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Rel I (Q) \leftrightarrow Rel \{⟨y, z⟩ \| (y = z (F) \land z \in TEndo (K) (W))\})$
15	11 14	mpbiri	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Rel I (Q)$
16		ssrab2	$⊢ \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} \subseteq T \times TEndo (K) (W)$
17		relxp	$⊢ Rel (T \times TEndo (K) (W))$
18		relss	$⊢ \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} \subseteq T \times TEndo (K) (W) \to (Rel (T \times TEndo (K) (W)) \to Rel \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\})$
19	16 17 18	mp2	$⊢ Rel \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
20	19	a1i	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Rel \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
21		id	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
22		vex	$⊢ g \in V$
23		vex	$⊢ s \in V$
24	1 2 3 4 5 12 6 9 22 23	dicopelval2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨g, s⟩ \in I (Q) \leftrightarrow (g = s (F) \land s \in TEndo (K) (W)))$
25		simprl	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to g = s (F)$
26		simpll	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to (K \in HL \land W \in H)$
27		simprr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to s \in TEndo (K) (W)$
28		simpl	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
29	1 2 3 4	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
30	29	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
31		simpr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
32	1 2 3 5 9	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
33	28 30 31 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
34	33	adantr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to F \in T$
35	3 5 12	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in TEndo (K) (W) \land F \in T) \to s (F) \in T$
36	26 27 34 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to s (F) \in T$
37	25 36	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to g \in T$
38	37 27 25	3jca	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g = s (F) \land s \in TEndo (K) (W))) \to (g \in T \land s \in TEndo (K) (W) \land g = s (F))$
39		simpr3	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g \in T \land s \in TEndo (K) (W) \land g = s (F))) \to g = s (F)$
40		simpr2	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g \in T \land s \in TEndo (K) (W) \land g = s (F))) \to s \in TEndo (K) (W)$
41	39 40	jca	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (g \in T \land s \in TEndo (K) (W) \land g = s (F))) \to (g = s (F) \land s \in TEndo (K) (W))$
42	38 41	impbida	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((g = s (F) \land s \in TEndo (K) (W)) \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land g = s (F)))$
43		eqid	$⊢ Scalar (U) = Scalar (U)$
44		eqid	$⊢ {Base}_{Scalar (U)} = {Base}_{Scalar (U)}$
45	3 12 7 43 44	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
46	45	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to {Base}_{Scalar (U)} = TEndo (K) (W)$
47	46	rexeqdv	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (\exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow \exists x \in TEndo (K) (W) ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)$
48		simpll	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (K \in HL \land W \in H)$
49		simpr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to x \in TEndo (K) (W)$
50	33	adantr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to F \in T$
51	3 5 12	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in TEndo (K) (W)$
52	51	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to {I ↾}_{T} \in TEndo (K) (W)$
53		eqid	$⊢ \cdot_{U} = \cdot_{U}$
54	3 5 12 7 53	dvhopvsca	$⊢ ((K \in HL \land W \in H) \land (x \in TEndo (K) (W) \land F \in T \land {I ↾}_{T} \in TEndo (K) (W))) \to x \cdot_{U} ⟨F, {I ↾}_{T}⟩ = ⟨x (F), x \circ ({I ↾}_{T})⟩$
55	48 49 50 52 54	syl13anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to x \cdot_{U} ⟨F, {I ↾}_{T}⟩ = ⟨x (F), x \circ ({I ↾}_{T})⟩$
56	55	eqeq2d	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow ⟨g, s⟩ = ⟨x (F), x \circ ({I ↾}_{T})⟩)$
57	22 23	opth	$⊢ ⟨g, s⟩ = ⟨x (F), x \circ ({I ↾}_{T})⟩ \leftrightarrow (g = x (F) \land s = x \circ ({I ↾}_{T}))$
58	56 57	bitrdi	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow (g = x (F) \land s = x \circ ({I ↾}_{T})))$
59	3 5 12	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land x \in TEndo (K) (W)) \to x \circ ({I ↾}_{T}) = x$
60	59	adantlr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to x \circ ({I ↾}_{T}) = x$
61	60	eqeq2d	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (s = x \circ ({I ↾}_{T}) \leftrightarrow s = x)$
62		equcom	$⊢ s = x \leftrightarrow x = s$
63	61 62	bitrdi	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (s = x \circ ({I ↾}_{T}) \leftrightarrow x = s)$
64	63	anbi2d	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to ((g = x (F) \land s = x \circ ({I ↾}_{T})) \leftrightarrow (g = x (F) \land x = s))$
65	58 64	bitrd	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow (g = x (F) \land x = s))$
66		ancom	$⊢ (g = x (F) \land x = s) \leftrightarrow (x = s \land g = x (F))$
67	65 66	bitrdi	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in TEndo (K) (W)) \to (⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow (x = s \land g = x (F)))$
68	67	rexbidva	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (\exists x \in TEndo (K) (W) ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow \exists x \in TEndo (K) (W) (x = s \land g = x (F)))$
69	47 68	bitrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (\exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow \exists x \in TEndo (K) (W) (x = s \land g = x (F)))$
70	69	3anbi3d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩) \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F))))$
71		fveq1	$⊢ x = s \to x (F) = s (F)$
72	71	eqeq2d	$⊢ x = s \to (g = x (F) \leftrightarrow g = s (F))$
73	72	ceqsrexv	$⊢ s \in TEndo (K) (W) \to (\exists x \in TEndo (K) (W) (x = s \land g = x (F)) \leftrightarrow g = s (F))$
74	73	pm5.32i	$⊢ (s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F))) \leftrightarrow (s \in TEndo (K) (W) \land g = s (F))$
75	74	anbi2i	$⊢ (g \in T \land (s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F)))) \leftrightarrow (g \in T \land (s \in TEndo (K) (W) \land g = s (F)))$
76		3anass	$⊢ (g \in T \land s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F))) \leftrightarrow (g \in T \land (s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F))))$
77		3anass	$⊢ (g \in T \land s \in TEndo (K) (W) \land g = s (F)) \leftrightarrow (g \in T \land (s \in TEndo (K) (W) \land g = s (F)))$
78	75 76 77	3bitr4i	$⊢ (g \in T \land s \in TEndo (K) (W) \land \exists x \in TEndo (K) (W) (x = s \land g = x (F))) \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land g = s (F))$
79	70 78	bitr2di	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((g \in T \land s \in TEndo (K) (W) \land g = s (F)) \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩))$
80	42 79	bitrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((g = s (F) \land s \in TEndo (K) (W)) \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩))$
81		eqeq1	$⊢ v = ⟨g, s⟩ \to (v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)$
82	81	rexbidv	$⊢ v = ⟨g, s⟩ \to (\exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)$
83	82	rabxp	$⊢ \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} = \{⟨g, s⟩ \| (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)\}$
84	83	eleq2i	$⊢ ⟨g, s⟩ \in \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} \leftrightarrow ⟨g, s⟩ \in \{⟨g, s⟩ \| (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)\}$
85		opabidw	$⊢ ⟨g, s⟩ \in \{⟨g, s⟩ \| (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)\} \leftrightarrow (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)$
86	84 85	bitr2i	$⊢ (g \in T \land s \in TEndo (K) (W) \land \exists x \in {Base}_{Scalar (U)} ⟨g, s⟩ = x \cdot_{U} ⟨F, {I ↾}_{T}⟩) \leftrightarrow ⟨g, s⟩ \in \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
87	80 86	bitrdi	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ((g = s (F) \land s \in TEndo (K) (W)) \leftrightarrow ⟨g, s⟩ \in \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\})$
88	24 87	bitrd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨g, s⟩ \in I (Q) \leftrightarrow ⟨g, s⟩ \in \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\})$
89	88	eqrelrdv2	$⊢ ((Rel I (Q) \land Rel \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}) \land ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to I (Q) = \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
90	15 20 21 89	syl21anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{v \in (T \times TEndo (K) (W)) \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
91		simpll	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in {Base}_{Scalar (U)}) \to (K \in HL \land W \in H)$
92	46	eleq2d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (x \in {Base}_{Scalar (U)} \leftrightarrow x \in TEndo (K) (W))$
93	92	biimpa	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in {Base}_{Scalar (U)}) \to x \in TEndo (K) (W)$
94	51	adantr	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to {I ↾}_{T} \in TEndo (K) (W)$
95		opelxpi	$⊢ (F \in T \land {I ↾}_{T} \in TEndo (K) (W)) \to ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W))$
96	33 94 95	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W))$
97	96	adantr	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in {Base}_{Scalar (U)}) \to ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W))$
98	3 5 12 7 53	dvhvscacl	$⊢ ((K \in HL \land W \in H) \land (x \in TEndo (K) (W) \land ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W)))) \to x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W))$
99	91 93 97 98	syl12anc	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in {Base}_{Scalar (U)}) \to x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W))$
100		eleq1a	$⊢ x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \in (T \times TEndo (K) (W)) \to (v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \to v \in (T \times TEndo (K) (W)))$
101	99 100	syl	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land x \in {Base}_{Scalar (U)}) \to (v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \to v \in (T \times TEndo (K) (W)))$
102	101	rexlimdva	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (\exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \to v \in (T \times TEndo (K) (W)))$
103	102	pm4.71rd	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (\exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩ \leftrightarrow (v \in (T \times TEndo (K) (W)) \land \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩))$
104	103	abbidv	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \{v \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\} = \{v \| (v \in (T \times TEndo (K) (W)) \land \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩)\}$
105	10 90 104	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{v \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
106	3 7 28	dvhlmod	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to U \in LMod$
107		eqid	$⊢ {Base}_{U} = {Base}_{U}$
108	3 5 12 7 107	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (F \in T \land {I ↾}_{T} \in TEndo (K) (W))) \to ⟨F, {I ↾}_{T}⟩ \in {Base}_{U}$
109	28 33 94 108	syl12anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to ⟨F, {I ↾}_{T}⟩ \in {Base}_{U}$
110	43 44 107 53 8	lspsn	$⊢ (U \in LMod \land ⟨F, {I ↾}_{T}⟩ \in {Base}_{U}) \to N (\{⟨F, {I ↾}_{T}⟩\}) = \{v \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
111	106 109 110	syl2anc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to N (\{⟨F, {I ↾}_{T}⟩\}) = \{v \| \exists x \in {Base}_{Scalar (U)} v = x \cdot_{U} ⟨F, {I ↾}_{T}⟩\}$
112	105 111	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = N (\{⟨F, {I ↾}_{T}⟩\})$

Metamath Proof Explorer

Theorem diclspsn

Proof