rrx2pnedifcoorneorr

Description: If two different points X and Y in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023)

	Ref	Expression
Hypotheses	rrx2pnecoorneor.i	\|- I = { 1 , 2 }
	rrx2pnecoorneor.b	\|- P = ( RR ^m I )
	rrx2pnedifcoorneor.a	\|- A = ( ( Y ` 1 ) - ( X ` 1 ) )
	rrx2pnedifcoorneorr.b	\|- B = ( ( X ` 2 ) - ( Y ` 2 ) )
Assertion	rrx2pnedifcoorneorr	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )

Proof

Step	Hyp	Ref	Expression
1		rrx2pnecoorneor.i	\|- I = { 1 , 2 }
2		rrx2pnecoorneor.b	\|- P = ( RR ^m I )
3		rrx2pnedifcoorneor.a	\|- A = ( ( Y ` 1 ) - ( X ` 1 ) )
4		rrx2pnedifcoorneorr.b	\|- B = ( ( X ` 2 ) - ( Y ` 2 ) )
5		eqid	\|- ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( Y ` 2 ) - ( X ` 2 ) )
6	1 2 3 5	rrx2pnedifcoorneor	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 ) )
7		eqcom	\|- ( ( Y ` 2 ) = ( X ` 2 ) <-> ( X ` 2 ) = ( Y ` 2 ) )
8	7	a1i	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 2 ) = ( X ` 2 ) <-> ( X ` 2 ) = ( Y ` 2 ) ) )
9	1 2	rrx2pyel	\|- ( X e. P -> ( X ` 2 ) e. RR )
10	9	recnd	\|- ( X e. P -> ( X ` 2 ) e. CC )
11	1 2	rrx2pyel	\|- ( Y e. P -> ( Y ` 2 ) e. RR )
12	11	recnd	\|- ( Y e. P -> ( Y ` 2 ) e. CC )
13	10 12	anim12i	\|- ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) e. CC /\ ( Y ` 2 ) e. CC ) )
14	13	ancomd	\|- ( ( X e. P /\ Y e. P ) -> ( ( Y ` 2 ) e. CC /\ ( X ` 2 ) e. CC ) )
15	14	3adant3	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 2 ) e. CC /\ ( X ` 2 ) e. CC ) )
16		subeq0	\|- ( ( ( Y ` 2 ) e. CC /\ ( X ` 2 ) e. CC ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> ( Y ` 2 ) = ( X ` 2 ) ) )
17	15 16	syl	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> ( Y ` 2 ) = ( X ` 2 ) ) )
18	13	3adant3	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( X ` 2 ) e. CC /\ ( Y ` 2 ) e. CC ) )
19		subeq0	\|- ( ( ( X ` 2 ) e. CC /\ ( Y ` 2 ) e. CC ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) = 0 <-> ( X ` 2 ) = ( Y ` 2 ) ) )
20	18 19	syl	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( X ` 2 ) - ( Y ` 2 ) ) = 0 <-> ( X ` 2 ) = ( Y ` 2 ) ) )
21	8 17 20	3bitr4d	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> ( ( X ` 2 ) - ( Y ` 2 ) ) = 0 ) )
22	4	eqcomi	\|- ( ( X ` 2 ) - ( Y ` 2 ) ) = B
23	22	eqeq1i	\|- ( ( ( X ` 2 ) - ( Y ` 2 ) ) = 0 <-> B = 0 )
24	21 23	bitrdi	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) = 0 <-> B = 0 ) )
25	24	necon3bid	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 <-> B =/= 0 ) )
26	25	orbi2d	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( A =/= 0 \/ ( ( Y ` 2 ) - ( X ` 2 ) ) =/= 0 ) <-> ( A =/= 0 \/ B =/= 0 ) ) )
27	6 26	mpbid	\|- ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )

Metamath Proof Explorer

Theorem rrx2pnedifcoorneorr

Proof