dvh4dimat

Description: There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015)

	Ref	Expression
Hypotheses	dvh4dimat.h	$⊢ H = LHyp (K)$
	dvh4dimat.u	$⊢ U = DVecH (K) (W)$
	dvh4dimat.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dvh4dimat.a	$⊢ A = LSAtoms (U)$
	dvh4dimat.k	$⊢ φ \to (K \in HL \land W \in H)$
	dvh4dimat.p	$⊢ φ \to P \in A$
	dvh4dimat.q	$⊢ φ \to Q \in A$
	dvh4dimat.r	$⊢ φ \to R \in A$
Assertion	dvh4dimat	$⊢ φ \to \exists s \in A \neg s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R$

Proof

Step	Hyp	Ref	Expression
1		dvh4dimat.h	$⊢ H = LHyp (K)$
2		dvh4dimat.u	$⊢ U = DVecH (K) (W)$
3		dvh4dimat.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
4		dvh4dimat.a	$⊢ A = LSAtoms (U)$
5		dvh4dimat.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dvh4dimat.p	$⊢ φ \to P \in A$
7		dvh4dimat.q	$⊢ φ \to Q \in A$
8		dvh4dimat.r	$⊢ φ \to R \in A$
9	5	simpld	$⊢ φ \to K \in HL$
10		eqid	$⊢ Atoms (K) = Atoms (K)$
11		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
12	10 1 2 11 4	dihlatat	$⊢ ((K \in HL \land W \in H) \land P \in A) \to {DIsoH (K) (W)}^{-1} (P) \in Atoms (K)$
13	5 6 12	syl2anc	$⊢ φ \to {DIsoH (K) (W)}^{-1} (P) \in Atoms (K)$
14	10 1 2 11 4	dihlatat	$⊢ ((K \in HL \land W \in H) \land Q \in A) \to {DIsoH (K) (W)}^{-1} (Q) \in Atoms (K)$
15	5 7 14	syl2anc	$⊢ φ \to {DIsoH (K) (W)}^{-1} (Q) \in Atoms (K)$
16	10 1 2 11 4	dihlatat	$⊢ ((K \in HL \land W \in H) \land R \in A) \to {DIsoH (K) (W)}^{-1} (R) \in Atoms (K)$
17	5 8 16	syl2anc	$⊢ φ \to {DIsoH (K) (W)}^{-1} (R) \in Atoms (K)$
18		eqid	$⊢ join (K) = join (K)$
19		eqid	$⊢ \leq_{K} = \leq_{K}$
20	18 19 10	3dim3	$⊢ (K \in HL \land ({DIsoH (K) (W)}^{-1} (P) \in Atoms (K) \land {DIsoH (K) (W)}^{-1} (Q) \in Atoms (K) \land {DIsoH (K) (W)}^{-1} (R) \in Atoms (K))) \to \exists r \in Atoms (K) \neg r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R))$
21	9 13 15 17 20	syl13anc	$⊢ φ \to \exists r \in Atoms (K) \neg r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R))$
22	5	adantr	$⊢ (φ \land r \in Atoms (K)) \to (K \in HL \land W \in H)$
23	1 2 11 4	dih1dimat	$⊢ ((K \in HL \land W \in H) \land P \in A) \to P \in ran DIsoH (K) (W)$
24	5 6 23	syl2anc	$⊢ φ \to P \in ran DIsoH (K) (W)$
25	1 11 2 3 4 5 24 7	dihsmatrn	$⊢ φ \to P \underset{˙}{\oplus} Q \in ran DIsoH (K) (W)$
26	25	adantr	$⊢ (φ \land r \in Atoms (K)) \to P \underset{˙}{\oplus} Q \in ran DIsoH (K) (W)$
27	8	adantr	$⊢ (φ \land r \in Atoms (K)) \to R \in A$
28	18 1 11 2 3 4 22 26 27	dihjat4	$⊢ (φ \land r \in Atoms (K)) \to (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (P \underset{˙}{\oplus} Q) join (K) {DIsoH (K) (W)}^{-1} (R))$
29	24	adantr	$⊢ (φ \land r \in Atoms (K)) \to P \in ran DIsoH (K) (W)$
30	7	adantr	$⊢ (φ \land r \in Atoms (K)) \to Q \in A$
31	18 1 11 2 3 4 22 29 30	dihjat6	$⊢ (φ \land r \in Atoms (K)) \to {DIsoH (K) (W)}^{-1} (P \underset{˙}{\oplus} Q) = {DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)$
32	31	fvoveq1d	$⊢ (φ \land r \in Atoms (K)) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (P \underset{˙}{\oplus} Q) join (K) {DIsoH (K) (W)}^{-1} (R)) = DIsoH (K) (W) (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R))$
33	28 32	eqtrd	$⊢ (φ \land r \in Atoms (K)) \to (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R = DIsoH (K) (W) (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R))$
34	33	sseq2d	$⊢ (φ \land r \in Atoms (K)) \to (DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R \leftrightarrow DIsoH (K) (W) (r) \subseteq DIsoH (K) (W) (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)))$
35		eqid	$⊢ {Base}_{K} = {Base}_{K}$
36	35 10	atbase	$⊢ r \in Atoms (K) \to r \in {Base}_{K}$
37	36	adantl	$⊢ (φ \land r \in Atoms (K)) \to r \in {Base}_{K}$
38	9	hllatd	$⊢ φ \to K \in Lat$
39	35 18 10	hlatjcl	$⊢ (K \in HL \land {DIsoH (K) (W)}^{-1} (P) \in Atoms (K) \land {DIsoH (K) (W)}^{-1} (Q) \in Atoms (K)) \to {DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q) \in {Base}_{K}$
40	9 13 15 39	syl3anc	$⊢ φ \to {DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q) \in {Base}_{K}$
41	35 10	atbase	$⊢ {DIsoH (K) (W)}^{-1} (R) \in Atoms (K) \to {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}$
42	17 41	syl	$⊢ φ \to {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}$
43	35 18	latjcl	$⊢ (K \in Lat \land {DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q) \in {Base}_{K} \land {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}) \to ({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}$
44	38 40 42 43	syl3anc	$⊢ φ \to ({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}$
45	44	adantr	$⊢ (φ \land r \in Atoms (K)) \to ({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}$
46	35 19 1 11	dihord	$⊢ ((K \in HL \land W \in H) \land r \in {Base}_{K} \land ({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R) \in {Base}_{K}) \to (DIsoH (K) (W) (r) \subseteq DIsoH (K) (W) (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)) \leftrightarrow r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)))$
47	22 37 45 46	syl3anc	$⊢ (φ \land r \in Atoms (K)) \to (DIsoH (K) (W) (r) \subseteq DIsoH (K) (W) (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)) \leftrightarrow r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)))$
48	34 47	bitr2d	$⊢ (φ \land r \in Atoms (K)) \to (r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)) \leftrightarrow DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
49	48	notbid	$⊢ (φ \land r \in Atoms (K)) \to (\neg r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)) \leftrightarrow \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
50	49	rexbidva	$⊢ φ \to (\exists r \in Atoms (K) \neg r \leq_{K} (({DIsoH (K) (W)}^{-1} (P) join (K) {DIsoH (K) (W)}^{-1} (Q)) join (K) {DIsoH (K) (W)}^{-1} (R)) \leftrightarrow \exists r \in Atoms (K) \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
51	21 50	mpbid	$⊢ φ \to \exists r \in Atoms (K) \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R$
52	10 1 2 11 4	dihatlat	$⊢ ((K \in HL \land W \in H) \land r \in Atoms (K)) \to DIsoH (K) (W) (r) \in A$
53	5 52	sylan	$⊢ (φ \land r \in Atoms (K)) \to DIsoH (K) (W) (r) \in A$
54	10 1 2 11 4	dihlatat	$⊢ ((K \in HL \land W \in H) \land s \in A) \to {DIsoH (K) (W)}^{-1} (s) \in Atoms (K)$
55	5 54	sylan	$⊢ (φ \land s \in A) \to {DIsoH (K) (W)}^{-1} (s) \in Atoms (K)$
56	5	adantr	$⊢ (φ \land s \in A) \to (K \in HL \land W \in H)$
57	1 2 11 4	dih1dimat	$⊢ ((K \in HL \land W \in H) \land s \in A) \to s \in ran DIsoH (K) (W)$
58	5 57	sylan	$⊢ (φ \land s \in A) \to s \in ran DIsoH (K) (W)$
59	1 11	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land s \in ran DIsoH (K) (W)) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (s)) = s$
60	56 58 59	syl2anc	$⊢ (φ \land s \in A) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (s)) = s$
61	60	eqcomd	$⊢ (φ \land s \in A) \to s = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (s))$
62		fveq2	$⊢ r = {DIsoH (K) (W)}^{-1} (s) \to DIsoH (K) (W) (r) = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (s))$
63	62	rspceeqv	$⊢ ({DIsoH (K) (W)}^{-1} (s) \in Atoms (K) \land s = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (s))) \to \exists r \in Atoms (K) s = DIsoH (K) (W) (r)$
64	55 61 63	syl2anc	$⊢ (φ \land s \in A) \to \exists r \in Atoms (K) s = DIsoH (K) (W) (r)$
65		sseq1	$⊢ s = DIsoH (K) (W) (r) \to (s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R \leftrightarrow DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
66	65	notbid	$⊢ s = DIsoH (K) (W) (r) \to (\neg s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R \leftrightarrow \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
67	66	adantl	$⊢ (φ \land s = DIsoH (K) (W) (r)) \to (\neg s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R \leftrightarrow \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
68	53 64 67	rexxfrd	$⊢ φ \to (\exists s \in A \neg s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R \leftrightarrow \exists r \in Atoms (K) \neg DIsoH (K) (W) (r) \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R)$
69	51 68	mpbird	$⊢ φ \to \exists s \in A \neg s \subseteq (P \underset{˙}{\oplus} Q) \underset{˙}{\oplus} R$

Metamath Proof Explorer

Theorem dvh4dimat

Proof