dochnoncon

Description: Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	dochnoncon.h	$⊢ H = LHyp (K)$
	dochnoncon.u	$⊢ U = DVecH (K) (W)$
	dochnoncon.s	$⊢ S = LSubSp (U)$
	dochnoncon.z	$⊢ \underset{˙}{0} = 0_{U}$
	dochnoncon.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
Assertion	dochnoncon	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		dochnoncon.h	$⊢ H = LHyp (K)$
2		dochnoncon.u	$⊢ U = DVecH (K) (W)$
3		dochnoncon.s	$⊢ S = LSubSp (U)$
4		dochnoncon.z	$⊢ \underset{˙}{0} = 0_{U}$
5		dochnoncon.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
6		eqid	$⊢ {Base}_{U} = {Base}_{U}$
7	6 3	lssss	$⊢ X \in S \to X \subseteq {Base}_{U}$
8	1 2 6 5	dochocss	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
9	7 8	sylan2	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
10	9	ssrind	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X)$
11		simpl	$⊢ ((K \in HL \land W \in H) \land X \in S) \to (K \in HL \land W \in H)$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
14		eqid	$⊢ LSubSp (U) = LSubSp (U)$
15	12 1 13 2 14	dihf11	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
16	15	adantr	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U)$
17		f1f1orn	$⊢ DIsoH (K) (W) : {Base}_{K} \underset{1-1}{⟶} LSubSp (U) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W)$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W)$
19	1 13 2 6 5	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{U}) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
20	7 19	sylan2	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
21	1 2 13 14	dihrnlss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (X) \in LSubSp (U)$
22	20 21	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (X) \in LSubSp (U)$
23	6 14	lssss	$⊢ \underset{˙}{⊥} (X) \in LSubSp (U) \to \underset{˙}{⊥} (X) \subseteq {Base}_{U}$
24	22 23	syl	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (X) \subseteq {Base}_{U}$
25	1 13 2 6 5	dochcl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq {Base}_{U}) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
26	24 25	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)$
27		f1ocnvdm	$⊢ (DIsoH (K) (W) : {Base}_{K} \underset{1-1 onto}{⟶} ran DIsoH (K) (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \in {Base}_{K}$
28	18 26 27	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \in {Base}_{K}$
29		hlop	$⊢ K \in HL \to K \in OP$
30	29	ad2antrr	$⊢ ((K \in HL \land W \in H) \land X \in S) \to K \in OP$
31		eqid	$⊢ oc (K) = oc (K)$
32	12 31	opoccl	$⊢ (K \in OP \land {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \in {Base}_{K}) \to oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \in {Base}_{K}$
33	30 28 32	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \in {Base}_{K}$
34		eqid	$⊢ meet (K) = meet (K)$
35	12 34 1 13	dihmeet	$⊢ ((K \in HL \land W \in H) \land {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \in {Base}_{K} \land oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \in {Base}_{K}) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) meet (K) oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \cap DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))))$
36	11 28 33 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) meet (K) oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \cap DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))))$
37		eqid	$⊢ 0. (K) = 0. (K)$
38	12 31 34 37	opnoncon	$⊢ (K \in OP \land {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \in {Base}_{K}) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) meet (K) oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) = 0. (K)$
39	30 28 38	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to {DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) meet (K) oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) = 0. (K)$
40	39	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) meet (K) oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = DIsoH (K) (W) (0. (K))$
41	36 40	eqtr3d	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \cap DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = DIsoH (K) (W) (0. (K))$
42	1 13	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
43	26 42	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
44	31 1 13 5	dochvalr	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))))$
45	26 44	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))))$
46	1 13 5	dochoc	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
47	20 46	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
48	45 47	eqtr3d	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = \underset{˙}{⊥} (X)$
49	43 48	ineq12d	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))) \cap DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))) = \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X)$
50	37 1 13 2 4	dih0	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) (0. (K)) = \{\underset{˙}{0}\}$
51	50	adantr	$⊢ ((K \in HL \land W \in H) \land X \in S) \to DIsoH (K) (W) (0. (K)) = \{\underset{˙}{0}\}$
52	41 49 51	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \cap \underset{˙}{⊥} (X) = \{\underset{˙}{0}\}$
53	10 52	sseqtrd	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) \subseteq \{\underset{˙}{0}\}$
54	1 2 11	dvhlmod	$⊢ ((K \in HL \land W \in H) \land X \in S) \to U \in LMod$
55		simpr	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \in S$
56	1 2 13 3	dihrnlss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (X) \in S$
57	20 56	syldan	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \underset{˙}{⊥} (X) \in S$
58	3	lssincl	$⊢ (U \in LMod \land X \in S \land \underset{˙}{⊥} (X) \in S) \to X \cap \underset{˙}{⊥} (X) \in S$
59	54 55 57 58	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) \in S$
60	4 3	lss0ss	$⊢ (U \in LMod \land X \cap \underset{˙}{⊥} (X) \in S) \to \{\underset{˙}{0}\} \subseteq X \cap \underset{˙}{⊥} (X)$
61	54 59 60	syl2anc	$⊢ ((K \in HL \land W \in H) \land X \in S) \to \{\underset{˙}{0}\} \subseteq X \cap \underset{˙}{⊥} (X)$
62	53 61	eqssd	$⊢ ((K \in HL \land W \in H) \land X \in S) \to X \cap \underset{˙}{⊥} (X) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem dochnoncon

Proof