diblsmopel

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

	Ref	Expression
Hypotheses	diblsmopel.b	$⊢ B = {Base}_{K}$
	diblsmopel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diblsmopel.h	$⊢ H = LHyp (K)$
	diblsmopel.t	$⊢ T = LTrn (K) (W)$
	diblsmopel.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
	diblsmopel.v	$⊢ V = DVecA (K) (W)$
	diblsmopel.u	$⊢ U = DVecH (K) (W)$
	diblsmopel.q	$⊢ \underset{˙}{\oplus} = LSSum (V)$
	diblsmopel.p	$⊢ \underset{˙}{✚} = LSSum (U)$
	diblsmopel.j	$⊢ J = DIsoA (K) (W)$
	diblsmopel.i	$⊢ I = DIsoB (K) (W)$
	diblsmopel.k	$⊢ φ \to (K \in HL \land W \in H)$
	diblsmopel.x	$⊢ φ \to (X \in B \land X \underset{˙}{\leq} W)$
	diblsmopel.y	$⊢ φ \to (Y \in B \land Y \underset{˙}{\leq} W)$
Assertion	diblsmopel	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{✚} I (Y)) \leftrightarrow (F \in (J (X) \underset{˙}{\oplus} J (Y)) \land S = O))$

Proof

Step	Hyp	Ref	Expression
1		diblsmopel.b	$⊢ B = {Base}_{K}$
2		diblsmopel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diblsmopel.h	$⊢ H = LHyp (K)$
4		diblsmopel.t	$⊢ T = LTrn (K) (W)$
5		diblsmopel.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6		diblsmopel.v	$⊢ V = DVecA (K) (W)$
7		diblsmopel.u	$⊢ U = DVecH (K) (W)$
8		diblsmopel.q	$⊢ \underset{˙}{\oplus} = LSSum (V)$
9		diblsmopel.p	$⊢ \underset{˙}{✚} = LSSum (U)$
10		diblsmopel.j	$⊢ J = DIsoA (K) (W)$
11		diblsmopel.i	$⊢ I = DIsoB (K) (W)$
12		diblsmopel.k	$⊢ φ \to (K \in HL \land W \in H)$
13		diblsmopel.x	$⊢ φ \to (X \in B \land X \underset{˙}{\leq} W)$
14		diblsmopel.y	$⊢ φ \to (Y \in B \land Y \underset{˙}{\leq} W)$
15		eqid	$⊢ LSubSp (U) = LSubSp (U)$
16	1 2 3 7 11 15	diblss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \in LSubSp (U)$
17	12 13 16	syl2anc	$⊢ φ \to I (X) \in LSubSp (U)$
18	1 2 3 7 11 15	diblss	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to I (Y) \in LSubSp (U)$
19	12 14 18	syl2anc	$⊢ φ \to I (Y) \in LSubSp (U)$
20		eqid	$⊢ +_{U} = +_{U}$
21	3 7 20 15 9	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{˙}{✚} I (Y)) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
22	12 17 19 21	syl3anc	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{✚} I (Y)) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
23		excom	$⊢ \exists y \exists z \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow \exists z \exists y \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)$
24	1 2 3 4 5 10 11	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨x, y⟩ \in I (X) \leftrightarrow (x \in J (X) \land y = O))$
25	12 13 24	syl2anc	$⊢ φ \to (⟨x, y⟩ \in I (X) \leftrightarrow (x \in J (X) \land y = O))$
26	1 2 3 4 5 10 11	dibopelval2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to (⟨z, w⟩ \in I (Y) \leftrightarrow (z \in J (Y) \land w = O))$
27	12 14 26	syl2anc	$⊢ φ \to (⟨z, w⟩ \in I (Y) \leftrightarrow (z \in J (Y) \land w = O))$
28	25 27	anbi12d	$⊢ φ \to ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \leftrightarrow ((x \in J (X) \land y = O) \land (z \in J (Y) \land w = O)))$
29		an4	$⊢ ((x \in J (X) \land y = O) \land (z \in J (Y) \land w = O)) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land (y = O \land w = O))$
30		ancom	$⊢ ((x \in J (X) \land z \in J (Y)) \land (y = O \land w = O)) \leftrightarrow ((y = O \land w = O) \land (x \in J (X) \land z \in J (Y)))$
31	29 30	bitri	$⊢ ((x \in J (X) \land y = O) \land (z \in J (Y) \land w = O)) \leftrightarrow ((y = O \land w = O) \land (x \in J (X) \land z \in J (Y)))$
32	28 31	bitrdi	$⊢ φ \to ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \leftrightarrow ((y = O \land w = O) \land (x \in J (X) \land z \in J (Y))))$
33	32	anbi1d	$⊢ φ \to (((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow (((y = O \land w = O) \land (x \in J (X) \land z \in J (Y))) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
34		anass	$⊢ (((y = O \land w = O) \land (x \in J (X) \land z \in J (Y))) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow ((y = O \land w = O) \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
35		df-3an	$⊢ (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)) \leftrightarrow ((y = O \land w = O) \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
36	34 35	bitr4i	$⊢ (((y = O \land w = O) \land (x \in J (X) \land z \in J (Y))) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩))$
37	33 36	bitrdi	$⊢ φ \to (((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)))$
38	37	2exbidv	$⊢ φ \to (\exists y \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow \exists y \exists w (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)))$
39	4	fvexi	$⊢ T \in V$
40	39	mptex	$⊢ (f \in T ⟼ {I ↾}_{B}) \in V$
41	5 40	eqeltri	$⊢ O \in V$
42		opeq2	$⊢ y = O \to ⟨x, y⟩ = ⟨x, O⟩$
43	42	oveq1d	$⊢ y = O \to ⟨x, y⟩ +_{U} ⟨z, w⟩ = ⟨x, O⟩ +_{U} ⟨z, w⟩$
44	43	eqeq2d	$⊢ y = O \to (⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩ \leftrightarrow ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, w⟩)$
45	44	anbi2d	$⊢ y = O \to (((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, w⟩))$
46		opeq2	$⊢ w = O \to ⟨z, w⟩ = ⟨z, O⟩$
47	46	oveq2d	$⊢ w = O \to ⟨x, O⟩ +_{U} ⟨z, w⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩$
48	47	eqeq2d	$⊢ w = O \to (⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, w⟩ \leftrightarrow ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩)$
49	48	anbi2d	$⊢ w = O \to (((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, w⟩) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩))$
50	41 41 45 49	ceqsex2v	$⊢ \exists y \exists w (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩)$
51	12	adantr	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (K \in HL \land W \in H)$
52	13	adantr	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (X \in B \land X \underset{˙}{\leq} W)$
53		simprl	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to x \in J (X)$
54	1 2 3 4 10	diael	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land x \in J (X)) \to x \in T$
55	51 52 53 54	syl3anc	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to x \in T$
56		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
57	1 3 4 56 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in TEndo (K) (W)$
58	51 57	syl	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to O \in TEndo (K) (W)$
59	14	adantr	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (Y \in B \land Y \underset{˙}{\leq} W)$
60		simprr	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to z \in J (Y)$
61	1 2 3 4 10	diael	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W) \land z \in J (Y)) \to z \in T$
62	51 59 60 61	syl3anc	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to z \in T$
63		eqid	$⊢ Scalar (U) = Scalar (U)$
64		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
65	3 4 56 7 63 20 64	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (x \in T \land O \in TEndo (K) (W)) \land (z \in T \land O \in TEndo (K) (W))) \to ⟨x, O⟩ +_{U} ⟨z, O⟩ = ⟨x \circ z, O +_{Scalar (U)} O⟩$
66	51 55 58 62 58 65	syl122anc	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to ⟨x, O⟩ +_{U} ⟨z, O⟩ = ⟨x \circ z, O +_{Scalar (U)} O⟩$
67	66	eqeq2d	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩ \leftrightarrow ⟨F, S⟩ = ⟨x \circ z, O +_{Scalar (U)} O⟩)$
68		vex	$⊢ x \in V$
69		vex	$⊢ z \in V$
70	68 69	coex	$⊢ x \circ z \in V$
71		ovex	$⊢ O +_{Scalar (U)} O \in V$
72	70 71	opth2	$⊢ ⟨F, S⟩ = ⟨x \circ z, O +_{Scalar (U)} O⟩ \leftrightarrow (F = x \circ z \land S = O +_{Scalar (U)} O)$
73		eqid	$⊢ +_{V} = +_{V}$
74	3 4 6 73	dvavadd	$⊢ ((K \in HL \land W \in H) \land (x \in T \land z \in T)) \to x +_{V} z = x \circ z$
75	51 55 62 74	syl12anc	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to x +_{V} z = x \circ z$
76	75	eqeq2d	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (F = x +_{V} z \leftrightarrow F = x \circ z)$
77	76	bicomd	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (F = x \circ z \leftrightarrow F = x +_{V} z)$
78		eqid	$⊢ (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f)))$
79	3 4 56 7 63 78 64	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f)))$
80	51 79	syl	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f)))$
81	80	oveqd	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to O +_{Scalar (U)} O = O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O$
82	1 3 4 56 5 78	tendo0pl	$⊢ ((K \in HL \land W \in H) \land O \in TEndo (K) (W)) \to O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O = O$
83	51 58 82	syl2anc	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O = O$
84	81 83	eqtrd	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to O +_{Scalar (U)} O = O$
85	84	eqeq2d	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (S = O +_{Scalar (U)} O \leftrightarrow S = O)$
86	77 85	anbi12d	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to ((F = x \circ z \land S = O +_{Scalar (U)} O) \leftrightarrow (F = x +_{V} z \land S = O))$
87	72 86	bitrid	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (⟨F, S⟩ = ⟨x \circ z, O +_{Scalar (U)} O⟩ \leftrightarrow (F = x +_{V} z \land S = O))$
88	67 87	bitrd	$⊢ (φ \land (x \in J (X) \land z \in J (Y))) \to (⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩ \leftrightarrow (F = x +_{V} z \land S = O))$
89	88	pm5.32da	$⊢ φ \to (((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, O⟩ +_{U} ⟨z, O⟩) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
90	50 89	bitrid	$⊢ φ \to (\exists y \exists w (y = O \land w = O \land ((x \in J (X) \land z \in J (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩)) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
91	38 90	bitrd	$⊢ φ \to (\exists y \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
92	91	exbidv	$⊢ φ \to (\exists z \exists y \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
93	23 92	bitrid	$⊢ φ \to (\exists y \exists z \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
94	93	exbidv	$⊢ φ \to (\exists x \exists y \exists z \exists w ((⟨x, y⟩ \in I (X) \land ⟨z, w⟩ \in I (Y)) \land ⟨F, S⟩ = ⟨x, y⟩ +_{U} ⟨z, w⟩) \leftrightarrow \exists x \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)))$
95		anass	$⊢ (((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O) \leftrightarrow ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O))$
96	95	bicomi	$⊢ ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)) \leftrightarrow (((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O)$
97	96	2exbii	$⊢ \exists x \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)) \leftrightarrow \exists x \exists z (((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O)$
98		19.41vv	$⊢ \exists x \exists z (((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O) \leftrightarrow (\exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O)$
99	97 98	bitri	$⊢ \exists x \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)) \leftrightarrow (\exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O)$
100	3 6	dvalvec	$⊢ (K \in HL \land W \in H) \to V \in LVec$
101		lveclmod	$⊢ V \in LVec \to V \in LMod$
102		eqid	$⊢ LSubSp (V) = LSubSp (V)$
103	102	lsssssubg	$⊢ V \in LMod \to LSubSp (V) \subseteq SubGrp (V)$
104	12 100 101 103	4syl	$⊢ φ \to LSubSp (V) \subseteq SubGrp (V)$
105	1 2 3 6 10 102	dialss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to J (X) \in LSubSp (V)$
106	12 13 105	syl2anc	$⊢ φ \to J (X) \in LSubSp (V)$
107	104 106	sseldd	$⊢ φ \to J (X) \in SubGrp (V)$
108	1 2 3 6 10 102	dialss	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land Y \underset{˙}{\leq} W)) \to J (Y) \in LSubSp (V)$
109	12 14 108	syl2anc	$⊢ φ \to J (Y) \in LSubSp (V)$
110	104 109	sseldd	$⊢ φ \to J (Y) \in SubGrp (V)$
111	73 8	lsmelval	$⊢ (J (X) \in SubGrp (V) \land J (Y) \in SubGrp (V)) \to (F \in (J (X) \underset{˙}{\oplus} J (Y)) \leftrightarrow \exists x \in J (X) \exists z \in J (Y) F = x +_{V} z)$
112	107 110 111	syl2anc	$⊢ φ \to (F \in (J (X) \underset{˙}{\oplus} J (Y)) \leftrightarrow \exists x \in J (X) \exists z \in J (Y) F = x +_{V} z)$
113		r2ex	$⊢ \exists x \in J (X) \exists z \in J (Y) F = x +_{V} z \leftrightarrow \exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z)$
114	112 113	bitrdi	$⊢ φ \to (F \in (J (X) \underset{˙}{\oplus} J (Y)) \leftrightarrow \exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z))$
115	114	anbi1d	$⊢ φ \to ((F \in (J (X) \underset{˙}{\oplus} J (Y)) \land S = O) \leftrightarrow (\exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O))$
116	115	bicomd	$⊢ φ \to ((\exists x \exists z ((x \in J (X) \land z \in J (Y)) \land F = x +_{V} z) \land S = O) \leftrightarrow (F \in (J (X) \underset{˙}{\oplus} J (Y)) \land S = O))$
117	99 116	bitrid	$⊢ φ \to (\exists x \exists z ((x \in J (X) \land z \in J (Y)) \land (F = x +_{V} z \land S = O)) \leftrightarrow (F \in (J (X) \underset{˙}{\oplus} J (Y)) \land S = O))$
118	22 94 117	3bitrd	$⊢ φ \to (⟨F, S⟩ \in (I (X) \underset{˙}{✚} I (Y)) \leftrightarrow (F \in (J (X) \underset{˙}{\oplus} J (Y)) \land S = O))$

Metamath Proof Explorer

Theorem diblsmopel

Proof