Theorem dochsatshp 39012

Description: The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.)

Hypotheses

Ref	Expression
dochsatshp.h	⊢ 𝐻 = (LHyp‘𝐾)
dochsatshp.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochsatshp.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
dochsatshp.a	⊢ 𝐴 = (LSAtoms‘𝑈)
dochsatshp.y	⊢ 𝑌 = (LSHyp‘𝑈)
dochsatshp.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dochsatshp.q	⊢ (𝜑 → 𝑄 ∈ 𝐴)

Assertion

Ref	Expression
dochsatshp	⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝑌)

Proof of Theorem dochsatshp

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dochsatshp.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		eqid 2759	. . . 4 ⊢ (Base‘𝑈) = (Base‘𝑈)
3		dochsatshp.a	. . . 4 ⊢ 𝐴 = (LSAtoms‘𝑈)
4		dochsatshp.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
5		dochsatshp.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6	4, 5, 1	dvhlmod 38671	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
7		dochsatshp.q	. . . 4 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
8	2, 3, 6, 7	lsatssv 36559	. . 3 ⊢ (𝜑 → 𝑄 ⊆ (Base‘𝑈))
9		eqid 2759	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
10		dochsatshp.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
11	4, 5, 2, 9, 10	dochlss 38915	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈))
12	1, 8, 11	syl2anc 588	. 2 ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈))
13		eqid 2759	. . . 4 ⊢ (0g‘𝑈) = (0g‘𝑈)
14	13, 3, 6, 7	lsatn0 36560	. . 3 ⊢ (𝜑 → 𝑄 ≠ {(0g‘𝑈)})
15	4, 5, 10, 2, 13	doch0 38919	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘{(0g‘𝑈)}) = (Base‘𝑈))
16	1, 15	syl 17	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{(0g‘𝑈)}) = (Base‘𝑈))
17	16	eqeq2d 2770	. . . . 5 ⊢ (𝜑 → (( ⊥ ‘𝑄) = ( ⊥ ‘{(0g‘𝑈)}) ↔ ( ⊥ ‘𝑄) = (Base‘𝑈)))
18		eqid 2759	. . . . . 6 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
19	4, 5, 18, 3	dih1dimat 38891	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊))
20	1, 7, 19	syl2anc 588	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊))
21	4, 18, 5, 13	dih0rn 38845	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → {(0g‘𝑈)} ∈ ran ((DIsoH‘𝐾)‘𝑊))
22	1, 21	syl 17	. . . . . 6 ⊢ (𝜑 → {(0g‘𝑈)} ∈ ran ((DIsoH‘𝐾)‘𝑊))
23	4, 18, 10, 1, 20, 22	doch11 38934	. . . . 5 ⊢ (𝜑 → (( ⊥ ‘𝑄) = ( ⊥ ‘{(0g‘𝑈)}) ↔ 𝑄 = {(0g‘𝑈)}))
24	17, 23	bitr3d 284	. . . 4 ⊢ (𝜑 → (( ⊥ ‘𝑄) = (Base‘𝑈) ↔ 𝑄 = {(0g‘𝑈)}))
25	24	necon3bid 2993	. . 3 ⊢ (𝜑 → (( ⊥ ‘𝑄) ≠ (Base‘𝑈) ↔ 𝑄 ≠ {(0g‘𝑈)}))
26	14, 25	mpbird 260	. 2 ⊢ (𝜑 → ( ⊥ ‘𝑄) ≠ (Base‘𝑈))
27		eqid 2759	. . . . . 6 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈)
28	2, 27, 13, 3	islsat 36552	. . . . 5 ⊢ (𝑈 ∈ LMod → (𝑄 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣})))
29	6, 28	syl 17	. . . 4 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣})))
30	7, 29	mpbid 235	. . 3 ⊢ (𝜑 → ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣}))
31		eldifi 4028	. . . . . . 7 ⊢ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) → 𝑣 ∈ (Base‘𝑈))
32	31	adantr 485	. . . . . 6 ⊢ ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → 𝑣 ∈ (Base‘𝑈))
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → 𝑣 ∈ (Base‘𝑈)))
34	9, 27	lspid 19807	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ LMod ∧ ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈)) → ((LSpan‘𝑈)‘( ⊥ ‘𝑄)) = ( ⊥ ‘𝑄))
35	6, 12, 34	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((LSpan‘𝑈)‘( ⊥ ‘𝑄)) = ( ⊥ ‘𝑄))
36	35	uneq1d 4063	. . . . . . . . . 10 ⊢ (𝜑 → (((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣})) = (( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))
37	36	fveq2d 6655	. . . . . . . . 9 ⊢ (𝜑 → ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))))
38	37	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))))
39	6	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → 𝑈 ∈ LMod)
40	2, 9	lssss 19761	. . . . . . . . . . 11 ⊢ (( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) → ( ⊥ ‘𝑄) ⊆ (Base‘𝑈))
41	12, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ( ⊥ ‘𝑄) ⊆ (Base‘𝑈))
42	41	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ( ⊥ ‘𝑄) ⊆ (Base‘𝑈))
43	31	snssd 4692	. . . . . . . . . . 11 ⊢ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) → {𝑣} ⊆ (Base‘𝑈))
44	43	adantr 485	. . . . . . . . . 10 ⊢ ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → {𝑣} ⊆ (Base‘𝑈))
45	44	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → {𝑣} ⊆ (Base‘𝑈))
46	2, 27	lspun 19812	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ ( ⊥ ‘𝑄) ⊆ (Base‘𝑈) ∧ {𝑣} ⊆ (Base‘𝑈)) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))))
47	39, 42, 45, 46	syl3anc 1369	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))))
48		uneq2 4058	. . . . . . . . . . 11 ⊢ (𝑄 = ((LSpan‘𝑈)‘{𝑣}) → (( ⊥ ‘𝑄) ∪ 𝑄) = (( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))
49	48	fveq2d 6655	. . . . . . . . . 10 ⊢ (𝑄 = ((LSpan‘𝑈)‘{𝑣}) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))))
50	49	adantl 486	. . . . . . . . 9 ⊢ ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))))
51	50	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))))
52	38, 47, 51	3eqtr4d 2804	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)))
53		eqid 2759	. . . . . . . . . . 11 ⊢ ((joinH‘𝐾)‘𝑊) = ((joinH‘𝐾)‘𝑊)
54		eqid 2759	. . . . . . . . . . 11 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
55	4, 18, 5, 2, 10	dochcl 38914	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊))
56	1, 8, 55	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊))
57	4, 18, 53, 5, 54, 3, 1, 56, 7	dihjat2 38992	. . . . . . . . . 10 ⊢ (𝜑 → (( ⊥ ‘𝑄)((joinH‘𝐾)‘𝑊)𝑄) = (( ⊥ ‘𝑄)(LSSum‘𝑈)𝑄))
58	4, 5, 2, 53, 1, 41, 8	djhcom 38966	. . . . . . . . . 10 ⊢ (𝜑 → (( ⊥ ‘𝑄)((joinH‘𝐾)‘𝑊)𝑄) = (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)))
59	9, 3, 6, 7	lsatlssel 36558	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (LSubSp‘𝑈))
60	9, 27, 54	lsmsp 19911	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) ∧ 𝑄 ∈ (LSubSp‘𝑈)) → (( ⊥ ‘𝑄)(LSSum‘𝑈)𝑄) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)))
61	6, 12, 59, 60	syl3anc 1369	. . . . . . . . . 10 ⊢ (𝜑 → (( ⊥ ‘𝑄)(LSSum‘𝑈)𝑄) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)))
62	57, 58, 61	3eqtr3rd 2803	. . . . . . . . 9 ⊢ (𝜑 → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)))
63	4, 5, 2, 10, 53	djhexmid 38972	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)) = (Base‘𝑈))
64	1, 8, 63	syl2anc 588	. . . . . . . . 9 ⊢ (𝜑 → (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)) = (Base‘𝑈))
65	62, 64	eqtrd 2794	. . . . . . . 8 ⊢ (𝜑 → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (Base‘𝑈))
66	65	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (Base‘𝑈))
67	52, 66	eqtrd 2794	. . . . . 6 ⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))
68	67	ex 417	. . . . 5 ⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)))
69	33, 68	jcad 517	. . . 4 ⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → (𝑣 ∈ (Base‘𝑈) ∧ ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))))
70	69	reximdv2 3193	. . 3 ⊢ (𝜑 → (∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣}) → ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)))
71	30, 70	mpd 15	. 2 ⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))
72	4, 5, 1	dvhlvec 38670	. . 3 ⊢ (𝜑 → 𝑈 ∈ LVec)
73		dochsatshp.y	. . . 4 ⊢ 𝑌 = (LSHyp‘𝑈)
74	2, 27, 9, 73	islshp 36540	. . 3 ⊢ (𝑈 ∈ LVec → (( ⊥ ‘𝑄) ∈ 𝑌 ↔ (( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) ∧ ( ⊥ ‘𝑄) ≠ (Base‘𝑈) ∧ ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))))
75	72, 74	syl 17	. 2 ⊢ (𝜑 → (( ⊥ ‘𝑄) ∈ 𝑌 ↔ (( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) ∧ ( ⊥ ‘𝑄) ≠ (Base‘𝑈) ∧ ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))))
76	12, 26, 71, 75	mpbir3and 1340	1 ⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝑌)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∃wrex 3069   ∖ cdif 3851   ∪ cun 3852   ⊆ wss 3854  {csn 4515  ran crn 5518  ‘cfv 6328  (class class class)co 7143  Basecbs 16526  0_gc0g 16756  LSSumclsm 18811  LModclmod 19687  LSubSpclss 19756  LSpanclspn 19796  LVecclvec 19927  LSAtomsclsa 36535  LSHypclsh 36536  HLchlt 36911  LHypclh 37545  DVecHcdvh 38639  DIsoHcdih 38789  ocHcoch 38908  joinHcdjh 38955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-riotaBAD 36514

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-om 7573  df-1st 7686  df-2nd 7687  df-tpos 7895  df-undef 7942  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-oadd 8109  df-er 8292  df-map 8411  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-n0 11920  df-z 12006  df-uz 12268  df-fz 12925  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-sca 16624  df-vsca 16625  df-0g 16758  df-proset 17589  df-poset 17607  df-plt 17619  df-lub 17635  df-glb 17636  df-join 17637  df-meet 17638  df-p0 17700  df-p1 17701  df-lat 17707  df-clat 17769  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-submnd 18008  df-grp 18157  df-minusg 18158  df-sbg 18159  df-subg 18328  df-cntz 18499  df-lsm 18813  df-cmn 18960  df-abl 18961  df-mgp 19293  df-ur 19305  df-ring 19352  df-oppr 19429  df-dvdsr 19447  df-unit 19448  df-invr 19478  df-dvr 19489  df-drng 19557  df-lmod 19689  df-lss 19757  df-lsp 19797  df-lvec 19928  df-lsatoms 36537  df-lshyp 36538  df-oposet 36737  df-ol 36739  df-oml 36740  df-covers 36827  df-ats 36828  df-atl 36859  df-cvlat 36883  df-hlat 36912  df-llines 37059  df-lplanes 37060  df-lvols 37061  df-lines 37062  df-psubsp 37064  df-pmap 37065  df-padd 37357  df-lhyp 37549  df-laut 37550  df-ldil 37665  df-ltrn 37666  df-trl 37720  df-tgrp 38304  df-tendo 38316  df-edring 38318  df-dveca 38564  df-disoa 38590  df-dvech 38640  df-dib 38700  df-dic 38734  df-dih 38790  df-doch 38909  df-djh 38956

This theorem is referenced by:  dochsatshpb  39013  dochsnshp  39014  dochpolN  39051  lclkrlem2c  39070  lclkrlem2e  39072  mapdordlem2  39198