dihopellsm

Description: Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dihopellsm.b	$⊢ B = {Base}_{K}$
	dihopellsm.h	$⊢ H = LHyp (K)$
	dihopellsm.t	$⊢ T = LTrn (K) (W)$
	dihopellsm.e	$⊢ E = TEndo (K) (W)$
	dihopellsm.a	$⊢ A = (v \in E, w \in E ⟼ (i \in T ⟼ v (i) \circ w (i)))$
	dihopellsm.u	$⊢ U = DVecH (K) (W)$
	dihopellsm.l	$⊢ L = LSubSp (U)$
	dihopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihopellsm.i	$⊢ I = DIsoH (K) (W)$
	dihopellsm.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihopellsm.x	$⊢ φ \to X \in B$
	dihopellsm.y	$⊢ φ \to Y \in B$
Assertion	dihopellsm	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{\oplus} I (Y)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land (F = g \circ h \land S = t A u)))$

Proof

Step	Hyp	Ref	Expression
1		dihopellsm.b	$⊢ B = {Base}_{K}$
2		dihopellsm.h	$⊢ H = LHyp (K)$
3		dihopellsm.t	$⊢ T = LTrn (K) (W)$
4		dihopellsm.e	$⊢ E = TEndo (K) (W)$
5		dihopellsm.a	$⊢ A = (v \in E, w \in E ⟼ (i \in T ⟼ v (i) \circ w (i)))$
6		dihopellsm.u	$⊢ U = DVecH (K) (W)$
7		dihopellsm.l	$⊢ L = LSubSp (U)$
8		dihopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		dihopellsm.i	$⊢ I = DIsoH (K) (W)$
10		dihopellsm.k	$⊢ φ \to (K \in HL \land W \in H)$
11		dihopellsm.x	$⊢ φ \to X \in B$
12		dihopellsm.y	$⊢ φ \to Y \in B$
13		eqid	$⊢ LSubSp (U) = LSubSp (U)$
14	1 2 9 6 13	dihlss	$⊢ ((K \in HL \land W \in H) \land X \in B) \to I (X) \in LSubSp (U)$
15	10 11 14	syl2anc	$⊢ φ \to I (X) \in LSubSp (U)$
16	1 2 9 6 13	dihlss	$⊢ ((K \in HL \land W \in H) \land Y \in B) \to I (Y) \in LSubSp (U)$
17	10 12 16	syl2anc	$⊢ φ \to I (Y) \in LSubSp (U)$
18		eqid	$⊢ +_{U} = +_{U}$
19	2 6 18 13 8	dvhopellsm	$⊢ ((K \in HL \land W \in H) \land I (X) \in LSubSp (U) \land I (Y) \in LSubSp (U)) \to (⟨F, S⟩ \in (I (X) \underset{˙}{\oplus} I (Y)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩))$
20	10 15 17 19	syl3anc	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{\oplus} I (Y)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩))$
21	10	adantr	$⊢ (φ \land ⟨g, t⟩ \in I (X)) \to (K \in HL \land W \in H)$
22	11	adantr	$⊢ (φ \land ⟨g, t⟩ \in I (X)) \to X \in B$
23		simpr	$⊢ (φ \land ⟨g, t⟩ \in I (X)) \to ⟨g, t⟩ \in I (X)$
24	1 2 3 4 9 21 22 23	dihopcl	$⊢ (φ \land ⟨g, t⟩ \in I (X)) \to (g \in T \land t \in E)$
25	10	adantr	$⊢ (φ \land ⟨h, u⟩ \in I (Y)) \to (K \in HL \land W \in H)$
26	12	adantr	$⊢ (φ \land ⟨h, u⟩ \in I (Y)) \to Y \in B$
27		simpr	$⊢ (φ \land ⟨h, u⟩ \in I (Y)) \to ⟨h, u⟩ \in I (Y)$
28	1 2 3 4 9 25 26 27	dihopcl	$⊢ (φ \land ⟨h, u⟩ \in I (Y)) \to (h \in T \land u \in E)$
29	24 28	anim12dan	$⊢ (φ \land (⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y))) \to ((g \in T \land t \in E) \land (h \in T \land u \in E))$
30	10	adantr	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to (K \in HL \land W \in H)$
31		simprl	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to (g \in T \land t \in E)$
32		simprr	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to (h \in T \land u \in E)$
33	2 3 4 5 6 18	dvhopvadd2	$⊢ ((K \in HL \land W \in H) \land (g \in T \land t \in E) \land (h \in T \land u \in E)) \to ⟨g, t⟩ +_{U} ⟨h, u⟩ = ⟨g \circ h, t A u⟩$
34	30 31 32 33	syl3anc	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to ⟨g, t⟩ +_{U} ⟨h, u⟩ = ⟨g \circ h, t A u⟩$
35	34	eqeq2d	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to (⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩ \leftrightarrow ⟨F, S⟩ = ⟨g \circ h, t A u⟩)$
36		vex	$⊢ g \in V$
37		vex	$⊢ h \in V$
38	36 37	coex	$⊢ g \circ h \in V$
39		ovex	$⊢ t A u \in V$
40	38 39	opth2	$⊢ ⟨F, S⟩ = ⟨g \circ h, t A u⟩ \leftrightarrow (F = g \circ h \land S = t A u)$
41	35 40	bitrdi	$⊢ (φ \land ((g \in T \land t \in E) \land (h \in T \land u \in E))) \to (⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩ \leftrightarrow (F = g \circ h \land S = t A u))$
42	29 41	syldan	$⊢ (φ \land (⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y))) \to (⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩ \leftrightarrow (F = g \circ h \land S = t A u))$
43	42	pm5.32da	$⊢ φ \to (((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩) \leftrightarrow ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land (F = g \circ h \land S = t A u)))$
44	43	4exbidv	$⊢ φ \to (\exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨g, t⟩ +_{U} ⟨h, u⟩) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land (F = g \circ h \land S = t A u)))$
45	20 44	bitrd	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{\oplus} I (Y)) \leftrightarrow \exists g \exists t \exists h \exists u ((⟨g, t⟩ \in I (X) \land ⟨h, u⟩ \in I (Y)) \land (F = g \circ h \land S = t A u)))$

Metamath Proof Explorer

Theorem dihopellsm

Proof