xihopellsmN

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

	Ref	Expression
Hypotheses	xihopellsm.b	$⊢ B = {Base}_{K}$
	xihopellsm.h	$⊢ H = LHyp (K)$
	xihopellsm.t	$⊢ T = LTrn (K) (W)$
	xihopellsm.e	$⊢ E = TEndo (K) (W)$
	xihopellsm.a	$⊢ A = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
	xihopellsm.u	$⊢ U = DVecH (K) (W)$
	xihopellsm.l	$⊢ L = LSubSp (U)$
	xihopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	xihopellsm.i	$⊢ I = DIsoH (K) (W)$
	xihopellsm.k	$⊢ φ \to (K \in HL \land W \in H)$
	xihopellsm.x	$⊢ φ \to X \in B$
	xihopellsm.y	$⊢ φ \to Y \in B$
Assertion	xihopellsmN	$⊢ φ \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		xihopellsm.b	$⊢ B = {Base}_{K}$
2		xihopellsm.h	$⊢ H = LHyp (K)$
3		xihopellsm.t	$⊢ T = LTrn (K) (W)$
4		xihopellsm.e	$⊢ E = TEndo (K) (W)$
5		xihopellsm.a	$⊢ A = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
6		xihopellsm.u	$⊢ U = DVecH (K) (W)$
7		xihopellsm.l	$⊢ L = LSubSp (U)$
8		xihopellsm.p	$⊢ \underset{˙}{\oplus} = LSSum (U)$
9		xihopellsm.i	$⊢ I = DIsoH (K) (W)$
10		xihopellsm.k	$⊢ φ \to (K \in HL \land W \in H)$
11		xihopellsm.x	$⊢ φ \to X \in B$
12		xihopellsm.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 xihopellsmN

Proof