dihatlat

Description: The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014)

	Ref	Expression
Hypotheses	dihatlat.a	$⊢ A = Atoms (K)$
	dihatlat.h	$⊢ H = LHyp (K)$
	dihatlat.u	$⊢ U = DVecH (K) (W)$
	dihatlat.i	$⊢ I = DIsoH (K) (W)$
	dihatlat.l	$⊢ L = LSAtoms (U)$
Assertion	dihatlat	$⊢ ((K \in HL \land W \in H) \land Q \in A) \to I (Q) \in L$

Proof

Step	Hyp	Ref	Expression
1		dihatlat.a	$⊢ A = Atoms (K)$
2		dihatlat.h	$⊢ H = LHyp (K)$
3		dihatlat.u	$⊢ U = DVecH (K) (W)$
4		dihatlat.i	$⊢ I = DIsoH (K) (W)$
5		dihatlat.l	$⊢ L = LSAtoms (U)$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
9		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
10		eqid	$⊢ LSpan (U) = LSpan (U)$
11	6 7 1 2 8 9 3 4 10	dih1dimb2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land Q \leq_{K} W)) \to \exists g \in LTrn (K) (W) (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}))$
12	11	anassrs	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W) \to \exists g \in LTrn (K) (W) (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}))$
13		simp3rr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})$
14		simp1l	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to (K \in HL \land W \in H)$
15	2 3 14	dvhlmod	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to U \in LMod$
16		simp3l	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to g \in LTrn (K) (W)$
17		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
18	6 2 8 17 9	tendo0cl	$⊢ (K \in HL \land W \in H) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W)$
19	14 18	syl	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W)$
20		eqid	$⊢ {Base}_{U} = {Base}_{U}$
21	2 8 17 3 20	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land (g \in LTrn (K) (W) \land (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in TEndo (K) (W))) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \in {Base}_{U}$
22	14 16 19 21	syl12anc	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \in {Base}_{U}$
23		simp3rl	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to g \neq {I ↾}_{{Base}_{K}}$
24	23	neneqd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to \neg g = {I ↾}_{{Base}_{K}}$
25	24	intnanrd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to \neg (g = {I ↾}_{{Base}_{K}} \land (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
26		vex	$⊢ g \in V$
27		fvex	$⊢ LTrn (K) (W) \in V$
28	27	mptex	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) \in V$
29	26 28	opth	$⊢ ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \leftrightarrow (g = {I ↾}_{{Base}_{K}} \land (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
30	29	necon3abii	$⊢ ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \neq ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \leftrightarrow \neg (g = {I ↾}_{{Base}_{K}} \land (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
31	25 30	sylibr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \neq ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
32		eqid	$⊢ 0_{U} = 0_{U}$
33	6 2 8 3 32 9	dvh0g	$⊢ (K \in HL \land W \in H) \to 0_{U} = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
34	14 33	syl	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to 0_{U} = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
35	31 34	neeqtrrd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \neq 0_{U}$
36	20 10 32 5	lsatlspsn2	$⊢ (U \in LMod \land ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \in {Base}_{U} \land ⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \neq 0_{U}) \to LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}) \in L$
37	15 22 35 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\}) \in L$
38	13 37	eqeltrd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to I (Q) \in L$
39	38	3expa	$⊢ ((((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W) \land (g \in LTrn (K) (W) \land (g \neq {I ↾}_{{Base}_{K}} \land I (Q) = LSpan (U) (\{⟨g, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩\})))) \to I (Q) \in L$
40	12 39	rexlimddv	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land Q \leq_{K} W) \to I (Q) \in L$
41		eqid	$⊢ oc (K) (W) = oc (K) (W)$
42		eqid	$⊢ (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) = (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q)$
43	7 1 2 41 8 4 3 10 42	dih1dimc	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \leq_{K} W)) \to I (Q) = LSpan (U) (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})$
44	43	anassrs	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to I (Q) = LSpan (U) (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\})$
45		simpll	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to (K \in HL \land W \in H)$
46	2 3 45	dvhlmod	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to U \in LMod$
47		eqid	$⊢ oc (K) = oc (K)$
48	7 47 1 2	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W)$
49	48	ad2antrr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W)$
50		simplr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to Q \in A$
51		simpr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to \neg Q \leq_{K} W$
52	7 1 2 8 42	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (oc (K) (W) \in A \land \neg oc (K) (W) \leq_{K} W) \land (Q \in A \land \neg Q \leq_{K} W)) \to (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W)$
53	45 49 50 51 52	syl112anc	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W)$
54	2 8 17	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W)$
55	54	ad2antrr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W)$
56	2 8 17 3 20	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land ((ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in LTrn (K) (W) \land {I ↾}_{LTrn (K) (W)} \in TEndo (K) (W))) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in {Base}_{U}$
57	45 53 55 56	syl12anc	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in {Base}_{U}$
58	6 2 8 17 9	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{LTrn (K) (W)} \neq (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
59	58	ad2antrr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to {I ↾}_{LTrn (K) (W)} \neq (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
60	59	neneqd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to \neg {I ↾}_{LTrn (K) (W)} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
61	60	intnand	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to \neg ((ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) = {I ↾}_{{Base}_{K}} \land {I ↾}_{LTrn (K) (W)} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
62		riotaex	$⊢ (ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) \in V$
63		resiexg	$⊢ LTrn (K) (W) \in V \to {I ↾}_{LTrn (K) (W)} \in V$
64	27 63	ax-mp	$⊢ {I ↾}_{LTrn (K) (W)} \in V$
65	62 64	opth	$⊢ ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \leftrightarrow ((ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) = {I ↾}_{{Base}_{K}} \land {I ↾}_{LTrn (K) (W)} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
66	65	necon3abii	$⊢ ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \neq ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩ \leftrightarrow \neg ((ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q) = {I ↾}_{{Base}_{K}} \land {I ↾}_{LTrn (K) (W)} = (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}))$
67	61 66	sylibr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \neq ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
68	33	ad2antrr	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to 0_{U} = ⟨{I ↾}_{{Base}_{K}}, (f \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})⟩$
69	67 68	neeqtrrd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \neq 0_{U}$
70	20 10 32 5	lsatlspsn2	$⊢ (U \in LMod \land ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \in {Base}_{U} \land ⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩ \neq 0_{U}) \to LSpan (U) (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\}) \in L$
71	46 57 69 70	syl3anc	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to LSpan (U) (\{⟨(ι f \in LTrn (K) (W) \| f (oc (K) (W)) = Q), {I ↾}_{LTrn (K) (W)}⟩\}) \in L$
72	44 71	eqeltrd	$⊢ (((K \in HL \land W \in H) \land Q \in A) \land \neg Q \leq_{K} W) \to I (Q) \in L$
73	40 72	pm2.61dan	$⊢ ((K \in HL \land W \in H) \land Q \in A) \to I (Q) \in L$

Metamath Proof Explorer

Theorem dihatlat

Proof