Theorem cdj3lem3

Description: Lemma for cdj3i . Value of the second-component function T . (Contributed by NM, 23-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdj3lem2.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
	cdj3lem2.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
	cdj3lem3.3	$$⊢T=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)\right)$$
Assertion	cdj3lem3	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C{+}_{ℎ}D\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		cdj3lem2.1	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
2		cdj3lem2.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		cdj3lem3.3	$$⊢T=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)\right)$$
4		incom	$$⊢A\cap B=B\cap A$$
5	4	eqeq1i	$$⊢A\cap B=0_{\mathscr{H}}\leftrightarrow B\cap A=0_{\mathscr{H}}$$
6	2	sheli	$$⊢D\in B\to D\in \mathscr{H}$$
7	1	sheli	$$⊢C\in A\to C\in \mathscr{H}$$
8		ax-hvcom	$$⊢\left(D\in \mathscr{H}\wedge C\in \mathscr{H}\right)\to D{+}_{ℎ}C=C{+}_{ℎ}D$$
9	6 7 8	syl2an	$$⊢\left(D\in B\wedge C\in A\right)\to D{+}_{ℎ}C=C{+}_{ℎ}D$$
10	9	fveq2d	$$⊢\left(D\in B\wedge C\in A\right)\to T\left(D{+}_{ℎ}C\right)=T\left(C{+}_{ℎ}D\right)$$
11	10	3adant3	$$⊢\left(D\in B\wedge C\in A\wedge B\cap A=0_{\mathscr{H}}\right)\to T\left(D{+}_{ℎ}C\right)=T\left(C{+}_{ℎ}D\right)$$
12	2 1	shscomi	$$⊢B{+}_{\mathscr{H}}A=A{+}_{\mathscr{H}}B$$
13	2	sheli	$$⊢w\in B\to w\in \mathscr{H}$$
14	1	sheli	$$⊢z\in A\to z\in \mathscr{H}$$
15		ax-hvcom	$$⊢\left(w\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to w{+}_{ℎ}z=z{+}_{ℎ}w$$
16	13 14 15	syl2an	$$⊢\left(w\in B\wedge z\in A\right)\to w{+}_{ℎ}z=z{+}_{ℎ}w$$
17	16	eqeq2d	$$⊢\left(w\in B\wedge z\in A\right)\to \left(x=w{+}_{ℎ}z\leftrightarrow x=z{+}_{ℎ}w\right)$$
18	17	rexbidva	$$⊢w\in B\to \left(\exists z\in Ax=w{+}_{ℎ}z\leftrightarrow \exists z\in Ax=z{+}_{ℎ}w\right)$$
19	18	riotabiia	$$⊢\left(\iota w\in B|\exists z\in Ax=w{+}_{ℎ}z\right)=\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)$$
20	12 19	mpteq12i	$$⊢\left(x\in \left(B{+}_{\mathscr{H}}A\right)⟼\left(\iota w\in B|\exists z\in Ax=w{+}_{ℎ}z\right)\right)=\left(x\in \left(A{+}_{\mathscr{H}}B\right)⟼\left(\iota w\in B|\exists z\in Ax=z{+}_{ℎ}w\right)\right)$$
21	3 20	eqtr4i	$$⊢T=\left(x\in \left(B{+}_{\mathscr{H}}A\right)⟼\left(\iota w\in B|\exists z\in Ax=w{+}_{ℎ}z\right)\right)$$
22	2 1 21	cdj3lem2	$$⊢\left(D\in B\wedge C\in A\wedge B\cap A=0_{\mathscr{H}}\right)\to T\left(D{+}_{ℎ}C\right)=D$$
23	11 22	eqtr3d	$$⊢\left(D\in B\wedge C\in A\wedge B\cap A=0_{\mathscr{H}}\right)\to T\left(C{+}_{ℎ}D\right)=D$$
24	5 23	syl3an3b	$$⊢\left(D\in B\wedge C\in A\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C{+}_{ℎ}D\right)=D$$
25	24	3com12	$$⊢\left(C\in A\wedge D\in B\wedge A\cap B=0_{\mathscr{H}}\right)\to T\left(C{+}_{ℎ}D\right)=D$$