Theorem diblsmopel 40771

Description: Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)

Hypotheses

Ref	Expression
diblsmopel.b	⊢ 𝐵 = (Base‘𝐾)
diblsmopel.l	⊢ ≤ = (le‘𝐾)
diblsmopel.h	⊢ 𝐻 = (LHyp‘𝐾)
diblsmopel.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
diblsmopel.o	⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
diblsmopel.v	⊢ 𝑉 = ((DVecA‘𝐾)‘𝑊)
diblsmopel.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
diblsmopel.q	⊢ ⊕ = (LSSum‘𝑉)
diblsmopel.p	⊢ ✚ = (LSSum‘𝑈)
diblsmopel.j	⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)
diblsmopel.i	⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
diblsmopel.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
diblsmopel.x	⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))
diblsmopel.y	⊢ (𝜑 → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊))

Assertion

Ref	Expression
diblsmopel	⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂)))

Distinct variable groups:   𝐵,𝑓   𝑓,𝐻   𝑓,𝐾   𝑇,𝑓   𝑓,𝑊

Allowed substitution hints:   𝜑(𝑓)   ✚ (𝑓)   ⊕ (𝑓)   𝑆(𝑓)   𝑈(𝑓)   𝐹(𝑓)   𝐼(𝑓)   𝐽(𝑓)   ≤ (𝑓)   𝑂(𝑓)   𝑉(𝑓)   𝑋(𝑓)   𝑌(𝑓)

Proof of Theorem diblsmopel

Dummy variables 𝑥 𝑤 𝑦 𝑧 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		diblsmopel.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		diblsmopel.x	. . . 4 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))
3		diblsmopel.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
4		diblsmopel.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
5		diblsmopel.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
6		diblsmopel.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		diblsmopel.i	. . . . 5 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
8		eqid 2725	. . . . 5 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
9	3, 4, 5, 6, 7, 8	diblss 40770	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈))
10	1, 2, 9	syl2anc 582	. . 3 ⊢ (𝜑 → (𝐼‘𝑋) ∈ (LSubSp‘𝑈))
11		diblsmopel.y	. . . 4 ⊢ (𝜑 → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊))
12	3, 4, 5, 6, 7, 8	diblss 40770	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈))
13	1, 11, 12	syl2anc 582	. . 3 ⊢ (𝜑 → (𝐼‘𝑌) ∈ (LSubSp‘𝑈))
14		eqid 2725	. . . 4 ⊢ (+g‘𝑈) = (+g‘𝑈)
15		diblsmopel.p	. . . 4 ⊢ ✚ = (LSSum‘𝑈)
16	5, 6, 14, 8, 15	dvhopellsm 40717	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ (LSubSp‘𝑈) ∧ (𝐼‘𝑌) ∈ (LSubSp‘𝑈)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
17	1, 10, 13, 16	syl3anc 1368	. 2 ⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
18		excom 2151	. . . 4 ⊢ (∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ∃𝑧∃𝑦∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)))
19		diblsmopel.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
20		diblsmopel.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
21		diblsmopel.j	. . . . . . . . . . . . 13 ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊)
22	3, 4, 5, 19, 20, 21, 7	dibopelval2 40745	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ↔ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂)))
23	1, 2, 22	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ↔ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂)))
24	3, 4, 5, 19, 20, 21, 7	dibopelval2 40745	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌) ↔ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)))
25	1, 11, 24	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌) ↔ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)))
26	23, 25	anbi12d 630	. . . . . . . . . 10 ⊢ (𝜑 → ((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂))))
27		an4 654	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂)))
28		ancom 459	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))))
29	27, 28	bitri 274	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑦 = 𝑂) ∧ (𝑧 ∈ (𝐽‘𝑌) ∧ 𝑤 = 𝑂)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))))
30	26, 29	bitrdi 286	. . . . . . . . 9 ⊢ (𝜑 → ((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)))))
31	30	anbi1d 629	. . . . . . . 8 ⊢ (𝜑 → (((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ (((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
32		anass 467	. . . . . . . . 9 ⊢ ((((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
33		df-3an 1086	. . . . . . . . 9 ⊢ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))) ↔ ((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
34	32, 33	bitr4i 277	. . . . . . . 8 ⊢ ((((𝑦 = 𝑂 ∧ 𝑤 = 𝑂) ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
35	31, 34	bitrdi 286	. . . . . . 7 ⊢ (𝜑 → (((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ (𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)))))
36	35	2exbidv 1919	. . . . . 6 ⊢ (𝜑 → (∃𝑦∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)))))
37	19	fvexi 6910	. . . . . . . . . 10 ⊢ 𝑇 ∈ V
38	37	mptex 7235	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
39	20, 38	eqeltri 2821	. . . . . . . 8 ⊢ 𝑂 ∈ V
40		opeq2 4876	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑂 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑂⟩)
41	40	oveq1d 7434	. . . . . . . . . 10 ⊢ (𝑦 = 𝑂 → (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩) = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))
42	41	eqeq2d 2736	. . . . . . . . 9 ⊢ (𝑦 = 𝑂 → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)))
43	42	anbi2d 628	. . . . . . . 8 ⊢ (𝑦 = 𝑂 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))))
44		opeq2 4876	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑂 → ⟨𝑧, 𝑤⟩ = ⟨𝑧, 𝑂⟩)
45	44	oveq2d 7435	. . . . . . . . . 10 ⊢ (𝑤 = 𝑂 → (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩) = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩))
46	45	eqeq2d 2736	. . . . . . . . 9 ⊢ (𝑤 = 𝑂 → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩)))
47	46	anbi2d 628	. . . . . . . 8 ⊢ (𝑤 = 𝑂 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩))))
48	39, 39, 43, 47	ceqsex2v 3520	. . . . . . 7 ⊢ (∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩)))
49	1	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
50	2	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))
51		simprl 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑥 ∈ (𝐽‘𝑋))
52	3, 4, 5, 19, 21	diael 40643	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑥 ∈ (𝐽‘𝑋)) → 𝑥 ∈ 𝑇)
53	49, 50, 51, 52	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑥 ∈ 𝑇)
54		eqid 2725	. . . . . . . . . . . . 13 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
55	3, 5, 19, 54, 20	tendo0cl 40390	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊))
56	49, 55	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊))
57	11	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊))
58		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑧 ∈ (𝐽‘𝑌))
59	3, 4, 5, 19, 21	diael 40643	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊) ∧ 𝑧 ∈ (𝐽‘𝑌)) → 𝑧 ∈ 𝑇)
60	49, 57, 58, 59	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → 𝑧 ∈ 𝑇)
61		eqid 2725	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
62		eqid 2725	. . . . . . . . . . . 12 ⊢ (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
63	5, 19, 54, 6, 61, 14, 62	dvhopvadd 40693	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (𝑧 ∈ 𝑇 ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊))) → (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩) = ⟨(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)⟩)
64	49, 53, 56, 60, 56, 63	syl122anc 1376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩) = ⟨(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)⟩)
65	64	eqeq2d 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)⟩))
66		vex 3465	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
67		vex 3465	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
68	66, 67	coex 7938	. . . . . . . . . . 11 ⊢ (𝑥 ∘ 𝑧) ∈ V
69		ovex 7452	. . . . . . . . . . 11 ⊢ (𝑂(+g‘(Scalar‘𝑈))𝑂) ∈ V
70	68, 69	opth2 5482	. . . . . . . . . 10 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂)))
71		diblsmopel.v	. . . . . . . . . . . . . . 15 ⊢ 𝑉 = ((DVecA‘𝐾)‘𝑊)
72		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (+g‘𝑉) = (+g‘𝑉)
73	5, 19, 71, 72	dvavadd 40615	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (𝑥(+g‘𝑉)𝑧) = (𝑥 ∘ 𝑧))
74	49, 53, 60, 73	syl12anc 835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑥(+g‘𝑉)𝑧) = (𝑥 ∘ 𝑧))
75	74	eqeq2d 2736	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐹 = (𝑥(+g‘𝑉)𝑧) ↔ 𝐹 = (𝑥 ∘ 𝑧)))
76	75	bicomd 222	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝐹 = (𝑥 ∘ 𝑧) ↔ 𝐹 = (𝑥(+g‘𝑉)𝑧)))
77		eqid 2725	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))
78	5, 19, 54, 6, 61, 77, 62	dvhfplusr 40684	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))))
79	49, 78	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (+g‘(Scalar‘𝑈)) = (𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))))
80	79	oveqd 7436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(+g‘(Scalar‘𝑈))𝑂) = (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂))
81	3, 5, 19, 54, 20, 77	tendo0pl 40391	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) → (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂) = 𝑂)
82	49, 56, 81	syl2anc 582	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(𝑠 ∈ ((TEndo‘𝐾)‘𝑊), 𝑡 ∈ ((TEndo‘𝐾)‘𝑊) ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))𝑂) = 𝑂)
83	80, 82	eqtrd 2765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑂(+g‘(Scalar‘𝑈))𝑂) = 𝑂)
84	83	eqeq2d 2736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂) ↔ 𝑆 = 𝑂))
85	76, 84	anbi12d 630	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑂(+g‘(Scalar‘𝑈))𝑂)) ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))
86	70, 85	bitrid 282	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑂(+g‘(Scalar‘𝑈))𝑂)⟩ ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))
87	65, 86	bitrd 278	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩) ↔ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))
88	87	pm5.32da 577	. . . . . . 7 ⊢ (𝜑 → (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑂⟩(+g‘𝑈)⟨𝑧, 𝑂⟩)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
89	48, 88	bitrid 282	. . . . . 6 ⊢ (𝜑 → (∃𝑦∃𝑤(𝑦 = 𝑂 ∧ 𝑤 = 𝑂 ∧ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩))) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
90	36, 89	bitrd 278	. . . . 5 ⊢ (𝜑 → (∃𝑦∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
91	90	exbidv 1916	. . . 4 ⊢ (𝜑 → (∃𝑧∃𝑦∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
92	18, 91	bitrid 282	. . 3 ⊢ (𝜑 → (∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
93	92	exbidv 1916	. 2 ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐼‘𝑋) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐼‘𝑌)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩(+g‘𝑈)⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂))))
94		anass 467	. . . . . 6 ⊢ ((((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ ((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)))
95	94	bicomi 223	. . . . 5 ⊢ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂))
96	95	2exbii 1843	. . . 4 ⊢ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ ∃𝑥∃𝑧(((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂))
97		19.41vv 1946	. . . 4 ⊢ (∃𝑥∃𝑧(((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂))
98	96, 97	bitri 274	. . 3 ⊢ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂))
99	5, 71	dvalvec 40626	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑉 ∈ LVec)
100		lveclmod 21003	. . . . . . . . 9 ⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod)
101		eqid 2725	. . . . . . . . . 10 ⊢ (LSubSp‘𝑉) = (LSubSp‘𝑉)
102	101	lsssssubg 20854	. . . . . . . . 9 ⊢ (𝑉 ∈ LMod → (LSubSp‘𝑉) ⊆ (SubGrp‘𝑉))
103	1, 99, 100, 102	4syl 19	. . . . . . . 8 ⊢ (𝜑 → (LSubSp‘𝑉) ⊆ (SubGrp‘𝑉))
104	3, 4, 5, 71, 21, 101	dialss 40646	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐽‘𝑋) ∈ (LSubSp‘𝑉))
105	1, 2, 104	syl2anc 582	. . . . . . . 8 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LSubSp‘𝑉))
106	103, 105	sseldd 3977	. . . . . . 7 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (SubGrp‘𝑉))
107	3, 4, 5, 71, 21, 101	dialss 40646	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐽‘𝑌) ∈ (LSubSp‘𝑉))
108	1, 11, 107	syl2anc 582	. . . . . . . 8 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LSubSp‘𝑉))
109	103, 108	sseldd 3977	. . . . . . 7 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (SubGrp‘𝑉))
110		diblsmopel.q	. . . . . . . 8 ⊢ ⊕ = (LSSum‘𝑉)
111	72, 110	lsmelval 19616	. . . . . . 7 ⊢ (((𝐽‘𝑋) ∈ (SubGrp‘𝑉) ∧ (𝐽‘𝑌) ∈ (SubGrp‘𝑉)) → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥 ∈ (𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧)))
112	106, 109, 111	syl2anc 582	. . . . . 6 ⊢ (𝜑 → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥 ∈ (𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧)))
113		r2ex 3185	. . . . . 6 ⊢ (∃𝑥 ∈ (𝐽‘𝑋)∃𝑧 ∈ (𝐽‘𝑌)𝐹 = (𝑥(+g‘𝑉)𝑧) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)))
114	112, 113	bitrdi 286	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ↔ ∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧))))
115	114	anbi1d 629	. . . 4 ⊢ (𝜑 → ((𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂) ↔ (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂)))
116	115	bicomd 222	. . 3 ⊢ (𝜑 → ((∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ 𝐹 = (𝑥(+g‘𝑉)𝑧)) ∧ 𝑆 = 𝑂) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂)))
117	98, 116	bitrid 282	. 2 ⊢ (𝜑 → (∃𝑥∃𝑧((𝑥 ∈ (𝐽‘𝑋) ∧ 𝑧 ∈ (𝐽‘𝑌)) ∧ (𝐹 = (𝑥(+g‘𝑉)𝑧) ∧ 𝑆 = 𝑂)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂)))
118	17, 93, 117	3bitrd 304	1 ⊢ (𝜑 → (⟨𝐹, 𝑆⟩ ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∃wrex 3059  Vcvv 3461   ⊆ wss 3944  ⟨cop 4636   class class class wbr 5149   ↦ cmpt 5232   I cid 5575   ↾ cres 5680   ∘ ccom 5682  ‘cfv 6549  (class class class)co 7419   ∈ cmpo 7421  Basecbs 17183  +_gcplusg 17236  Scalarcsca 17239  lecple 17243  SubGrpcsubg 19083  LSSumclsm 19601  LModclmod 20755  LSubSpclss 20827  LVecclvec 20999  HLchlt 38949  LHypclh 39584  LTrncltrn 39701  TEndoctendo 40352  DVecAcdveca 40602  DIsoAcdia 40628  DVecHcdvh 40678  DIsoBcdib 40738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-riotaBAD 38552

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-tpos 8232  df-undef 8279  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-n0 12506  df-z 12592  df-uz 12856  df-fz 13520  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-sca 17252  df-vsca 17253  df-0g 17426  df-proset 18290  df-poset 18308  df-plt 18325  df-lub 18341  df-glb 18342  df-join 18343  df-meet 18344  df-p0 18420  df-p1 18421  df-lat 18427  df-clat 18494  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-grp 18901  df-minusg 18902  df-sbg 18903  df-subg 19086  df-lsm 19603  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-oppr 20285  df-dvdsr 20308  df-unit 20309  df-invr 20339  df-dvr 20352  df-drng 20638  df-lmod 20757  df-lss 20828  df-lvec 21000  df-oposet 38775  df-ol 38777  df-oml 38778  df-covers 38865  df-ats 38866  df-atl 38897  df-cvlat 38921  df-hlat 38950  df-llines 39098  df-lplanes 39099  df-lvols 39100  df-lines 39101  df-psubsp 39103  df-pmap 39104  df-padd 39396  df-lhyp 39588  df-laut 39589  df-ldil 39704  df-ltrn 39705  df-trl 39759  df-tgrp 40343  df-tendo 40355  df-edring 40357  df-dveca 40603  df-disoa 40629  df-dvech 40679  df-dib 40739

This theorem is referenced by:  dib2dim  40843  dih2dimbALTN  40845